From 8ff961cf205dce21cd81311cba4230ac068bd6cb Mon Sep 17 00:00:00 2001 From: Joseph Edwards Date: Mon, 1 Jun 2026 19:37:50 +0100 Subject: [PATCH 1/7] Restructure worksheet --- .../gap-solutions/problem-1.gap | 0 .../gap-solutions/problem-2.gap | 0 .../gap-solutions/problem-3.gap | 0 .../gap-solutions/problem-4.gap | 0 .../gap-solutions/problem-5.gap | 0 .../gap-solutions/problem-6.gap | 0 .../gap-solutions/problem-7.gap | 0 .../gap-solutions/problem-8.gap | 0 .../python-solutions/problem_1.py | 0 .../python-solutions/problem_2.py | 0 .../python-solutions/problem_3.py | 0 .../python-solutions/problem_4.py | 0 .../python-solutions/problem_5.py | 0 .../python-solutions/problem_6.py | 0 worksheet.pdf => worksheet/worksheet.pdf | Bin worksheet.tex => worksheet/worksheet.tex | 0 16 files changed, 0 insertions(+), 0 deletions(-) rename problem-1.gap => worksheet/gap-solutions/problem-1.gap (100%) rename problem-2.gap => worksheet/gap-solutions/problem-2.gap (100%) rename problem-3.gap => worksheet/gap-solutions/problem-3.gap (100%) rename problem-4.gap => worksheet/gap-solutions/problem-4.gap (100%) rename problem-5.gap => worksheet/gap-solutions/problem-5.gap (100%) rename problem-6.gap => worksheet/gap-solutions/problem-6.gap (100%) rename problem-7.gap => worksheet/gap-solutions/problem-7.gap (100%) rename problem-8.gap => worksheet/gap-solutions/problem-8.gap (100%) rename problem_1.py => worksheet/python-solutions/problem_1.py (100%) rename problem_2.py => worksheet/python-solutions/problem_2.py (100%) rename problem_3.py => worksheet/python-solutions/problem_3.py (100%) rename problem_4.py => worksheet/python-solutions/problem_4.py (100%) rename problem_5.py => worksheet/python-solutions/problem_5.py (100%) rename problem_6.py => worksheet/python-solutions/problem_6.py (100%) rename worksheet.pdf => worksheet/worksheet.pdf (100%) rename worksheet.tex => worksheet/worksheet.tex (100%) diff --git a/problem-1.gap b/worksheet/gap-solutions/problem-1.gap similarity index 100% rename from problem-1.gap rename to worksheet/gap-solutions/problem-1.gap diff --git a/problem-2.gap b/worksheet/gap-solutions/problem-2.gap similarity index 100% rename from problem-2.gap rename to worksheet/gap-solutions/problem-2.gap diff --git a/problem-3.gap b/worksheet/gap-solutions/problem-3.gap similarity index 100% rename from problem-3.gap rename to worksheet/gap-solutions/problem-3.gap diff --git a/problem-4.gap b/worksheet/gap-solutions/problem-4.gap similarity index 100% rename from problem-4.gap rename to worksheet/gap-solutions/problem-4.gap diff --git a/problem-5.gap b/worksheet/gap-solutions/problem-5.gap similarity index 100% rename from problem-5.gap rename to worksheet/gap-solutions/problem-5.gap diff --git a/problem-6.gap b/worksheet/gap-solutions/problem-6.gap similarity index 100% rename from problem-6.gap rename to worksheet/gap-solutions/problem-6.gap diff --git a/problem-7.gap b/worksheet/gap-solutions/problem-7.gap similarity index 100% rename from problem-7.gap rename to worksheet/gap-solutions/problem-7.gap diff --git a/problem-8.gap b/worksheet/gap-solutions/problem-8.gap similarity index 100% rename from problem-8.gap rename to worksheet/gap-solutions/problem-8.gap diff --git a/problem_1.py b/worksheet/python-solutions/problem_1.py similarity index 100% rename from problem_1.py rename to worksheet/python-solutions/problem_1.py diff --git a/problem_2.py b/worksheet/python-solutions/problem_2.py similarity index 100% rename from problem_2.py rename to worksheet/python-solutions/problem_2.py diff --git a/problem_3.py b/worksheet/python-solutions/problem_3.py similarity index 100% rename from problem_3.py rename to worksheet/python-solutions/problem_3.py diff --git a/problem_4.py b/worksheet/python-solutions/problem_4.py similarity index 100% rename from problem_4.py rename to worksheet/python-solutions/problem_4.py diff --git a/problem_5.py b/worksheet/python-solutions/problem_5.py similarity index 100% rename from problem_5.py rename to worksheet/python-solutions/problem_5.py diff --git a/problem_6.py b/worksheet/python-solutions/problem_6.py similarity index 100% rename from problem_6.py rename to worksheet/python-solutions/problem_6.py diff --git a/worksheet.pdf b/worksheet/worksheet.pdf similarity index 100% rename from worksheet.pdf rename to worksheet/worksheet.pdf diff --git a/worksheet.tex b/worksheet/worksheet.tex similarity index 100% rename from worksheet.tex rename to worksheet/worksheet.tex From 9374a05171decba92f19e693f0cf3d6e49ad2625 Mon Sep 17 00:00:00 2001 From: Joseph Edwards Date: Mon, 1 Jun 2026 19:39:25 +0100 Subject: [PATCH 2/7] Rename case-studies -> examples --- docs/case-studies/index.md | 9 --------- docs/{case-studies => examples}/cong-latt.md | 0 docs/{case-studies => examples}/gis.md | 0 docs/examples/index.md | 13 +++++++++++++ docs/{case-studies => examples}/short.md | 0 docs/{case-studies => examples}/stephen.md | 0 docs/{case-studies => examples}/trans-rep.md | 0 7 files changed, 13 insertions(+), 9 deletions(-) delete mode 100644 docs/case-studies/index.md rename docs/{case-studies => examples}/cong-latt.md (100%) rename docs/{case-studies => examples}/gis.md (100%) create mode 100644 docs/examples/index.md rename docs/{case-studies => examples}/short.md (100%) rename docs/{case-studies => examples}/stephen.md (100%) rename docs/{case-studies => examples}/trans-rep.md (100%) diff --git a/docs/case-studies/index.md b/docs/case-studies/index.md deleted file mode 100644 index 1cf0262..0000000 --- a/docs/case-studies/index.md +++ /dev/null @@ -1,9 +0,0 @@ -# Case studies - -This page contains links to various case studies of how the [Semigroups -package for GAP][] and/or [libsemigroups_pybind11][] have been used in -mathematical research. - -Please use the menu at the left or the links below: - -* [Short presentations for transformation monoids](short.md) diff --git a/docs/case-studies/cong-latt.md b/docs/examples/cong-latt.md similarity index 100% rename from docs/case-studies/cong-latt.md rename to docs/examples/cong-latt.md diff --git a/docs/case-studies/gis.md b/docs/examples/gis.md similarity index 100% rename from docs/case-studies/gis.md rename to docs/examples/gis.md diff --git a/docs/examples/index.md b/docs/examples/index.md new file mode 100644 index 0000000..e258f97 --- /dev/null +++ b/docs/examples/index.md @@ -0,0 +1,13 @@ +# Examples + +This page contains various links that explain how the +[Semigroups package for GAP][] and/or [libsemigroups_pybind11][] have been used +to conduct mathematical research. + +Please use the menu at the left or the links below: + +- [Short presentations for transformation monoids](short.md) +- [Verifying presentations in the ATLAS of Finite Groups](atlas/index.md) + +[Semigroups package for GAP]: https://semigroups.github.io/Semigroups/ +[libsemigroups_pybind11]: https://libsemigroups.github.io/libsemigroups_pybind11/index.html diff --git a/docs/case-studies/short.md b/docs/examples/short.md similarity index 100% rename from docs/case-studies/short.md rename to docs/examples/short.md diff --git a/docs/case-studies/stephen.md b/docs/examples/stephen.md similarity index 100% rename from docs/case-studies/stephen.md rename to docs/examples/stephen.md diff --git a/docs/case-studies/trans-rep.md b/docs/examples/trans-rep.md similarity index 100% rename from docs/case-studies/trans-rep.md rename to docs/examples/trans-rep.md From 20bc262690e1068466bd06e4681c59d80c26cd53 Mon Sep 17 00:00:00 2001 From: Joseph Edwards Date: Mon, 1 Jun 2026 19:39:46 +0100 Subject: [PATCH 3/7] Add atlas pages --- docs/examples/atlas/index.md | 185 ++++++ .../examples/atlas/leech-lattice/co2/index.md | 13 + docs/examples/atlas/leech-lattice/hs.md | 16 + docs/examples/atlas/leech-lattice/j2.md | 16 + .../examples/atlas/leech-lattice/mcl/index.md | 13 + docs/examples/atlas/mathieu/m11.md | 94 +++ docs/examples/atlas/mathieu/m12.md | 142 +++++ docs/examples/atlas/mathieu/m22.md | 565 ++++++++++++++++++ docs/examples/atlas/mathieu/m23/index.md | 13 + docs/examples/atlas/mathieu/m24/index.md | 13 + docs/examples/atlas/misc/t.md | 17 + .../atlas/monster-sections/fi22/index.md | 13 + .../atlas/monster-sections/he/index.md | 13 + docs/examples/atlas/pariahs/j1.md | 16 + docs/examples/atlas/pariahs/j3.md | 16 + docs/examples/atlas/pariahs/j4/index.md | 13 + docs/examples/atlas/pariahs/ru/index.md | 13 + docs/stylesheets/extra.css | 47 ++ mkdocs.yml | 44 +- 19 files changed, 1259 insertions(+), 3 deletions(-) create mode 100644 docs/examples/atlas/index.md create mode 100644 docs/examples/atlas/leech-lattice/co2/index.md create mode 100644 docs/examples/atlas/leech-lattice/hs.md create mode 100644 docs/examples/atlas/leech-lattice/j2.md create mode 100644 docs/examples/atlas/leech-lattice/mcl/index.md create mode 100644 docs/examples/atlas/mathieu/m11.md create mode 100644 docs/examples/atlas/mathieu/m12.md create mode 100644 docs/examples/atlas/mathieu/m22.md create mode 100644 docs/examples/atlas/mathieu/m23/index.md create mode 100644 docs/examples/atlas/mathieu/m24/index.md create mode 100644 docs/examples/atlas/misc/t.md create mode 100644 docs/examples/atlas/monster-sections/fi22/index.md create mode 100644 docs/examples/atlas/monster-sections/he/index.md create mode 100644 docs/examples/atlas/pariahs/j1.md create mode 100644 docs/examples/atlas/pariahs/j3.md create mode 100644 docs/examples/atlas/pariahs/j4/index.md create mode 100644 docs/examples/atlas/pariahs/ru/index.md create mode 100644 docs/stylesheets/extra.css diff --git a/docs/examples/atlas/index.md b/docs/examples/atlas/index.md new file mode 100644 index 0000000..5c19066 --- /dev/null +++ b/docs/examples/atlas/index.md @@ -0,0 +1,185 @@ +# Verifying presentations in the ATLAS of Finite Groups + +In this example, we will verify the validity of the presentations of the +sporadic groups as given in [this ATLAS][atlas]. +In particular, where possible, we will use the Todd-Coxeter algorithm to check +that the size of group defined by the presentations is equal to the claimed +size. Where the claimed size of the group is very large, we will instead +calculate the size of small-index subgroups. + +??? info "libsemigroups_pybind11 version" + + All examples provided on the subsequent subpages were run using + libsemigroups_pybind11 version 1.4.4 on a laptop with a 13th Gen Intel(R) + Core(TM) i7-13700H processor and 64 GB RAM. + +??? info "Defining groups with monoid presentations" + + The presentations provided for the groups in the ATLAS are + *group presentations*. This means that it is assumed that there is + multiplicative identity $1$, and that each generator $a$ has an inverse + $a^{-1}$ such that $aa^{-1} = a^{-1}a = 1$. In [libsemigroups_pybind11][], + however, presentations are either *semigroup presentations* or + *monoid presentations*, depending whether the relations of the presentation + are allowed to contain the empty word $\varepsilon$. Therefore, we will need + to add extra generators and relations to a monoid presentation to define a + group. + + Suppose that a group $G$ is defined by the group presentation + $\langle{A \mid R }\rangle_{\text{grp}}$. Then $G$ can also be defined by + the monoid presentation + $\langle{A \sqcup A^{-1} \mid R \cup R' }\rangle_{\text{mon}}$ where + $A^{-1}$ is a set disjoint from $A$ containing letters that will be treated + as inverses for the letters in $A$, and $R'$ is the set of relations of the + form $aa^{-1} = \varepsilon$ and $a^{-1}a = \varepsilon$. + + In the subsequent subpages, we will use lowercase letters for the + generators that are given in the presentations in the ATLAS, and their + uppercase counterparts to represent their inverses. Therefore, many of our + examples will in a similar way to: + + ```py + from libsemigroups_pybind11 import presentation, Presentation + p = presentation("abAB") + p.contains_empty_word(True) + presentation.add_inverse_rules(p, "ABab") + ``` + + The algorithms in [libsemigroups_pybind11][] were written for semigroups and + monoids. This means that there are no group-specific optimisations. + +The following tables summarise the results of this project. Click on a group +to see more information. + +
+
+
+ + + + + + + + + + + +
Mathieu groups
+ M11 + + M12 + + M22 + + M23 + + M24 +
+
+
+ + + + + + + + + + + + + +
Leech lattice groups
HS + J2 + Co1 + Co2 + Co3McLSuz
+
+
+ + + + + + + + + + + + + + +
Monster sections
HeHNTh + Fi22 + Fi23Fi24'BM
+
+
+ + + + + + + + + + + + +
Pariahs
+ J1 + O'N + J3 + Ru + J4 + Ly
+
+
+ + + + + + + +
Miscellaneous
T
+
+
+ +
+
+ + + + + + + + + + + + + + + + + + + +
Legend
+ The presentation defines a group of the correct size +
+ The presentation has a subgroup of the correct size +
+ The presentation defines a group of the incorrect size +
Todd-Coxeter did not terminate
No presentation is provided
+
+
+
+ +[atlas]: https://brauer.maths.qmul.ac.uk/Atlas/v3/spor/ +[libsemigroups_pybind11]: https://libsemigroups.github.io/libsemigroups_pybind11/index.html diff --git a/docs/examples/atlas/leech-lattice/co2/index.md b/docs/examples/atlas/leech-lattice/co2/index.md new file mode 100644 index 0000000..e781f66 --- /dev/null +++ b/docs/examples/atlas/leech-lattice/co2/index.md @@ -0,0 +1,13 @@ +# Conway group Co~2~ + +> Order: $42,305,421,312,000$ + +> Presentation: $\langle{ A \mid R}\rangle$ + +On this page, we provide links to verifications that the maximal subgroups of +the Conway group Co~2~ define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: + diff --git a/docs/examples/atlas/leech-lattice/hs.md b/docs/examples/atlas/leech-lattice/hs.md new file mode 100644 index 0000000..78b5fbf --- /dev/null +++ b/docs/examples/atlas/leech-lattice/hs.md @@ -0,0 +1,16 @@ +# Higman-Sims group HS + +> Order: $44,352,000$ + +> Presentation: $\langle{ A \mid R}\rangle$ + +On this page, we verify that the above claimed presentation of the Higman-Sims +group HS defines a group of order $44,352,000$. + +## The code + +Coming soon! + +## The output + +Coming soon! diff --git a/docs/examples/atlas/leech-lattice/j2.md b/docs/examples/atlas/leech-lattice/j2.md new file mode 100644 index 0000000..691fbd6 --- /dev/null +++ b/docs/examples/atlas/leech-lattice/j2.md @@ -0,0 +1,16 @@ +# Janko group J~2~ + +> Order: $604,800$ + +> Presentation: $\langle{ A \mid R}\rangle$ + +On this page, we verify that the above claimed presentation of the Janko group +J~2~ defines a group of order $604,800$. + +## The code + +Coming soon! + +## The output + +Coming soon! diff --git a/docs/examples/atlas/leech-lattice/mcl/index.md b/docs/examples/atlas/leech-lattice/mcl/index.md new file mode 100644 index 0000000..4abe0a4 --- /dev/null +++ b/docs/examples/atlas/leech-lattice/mcl/index.md @@ -0,0 +1,13 @@ +# McLaughlin group McL + +> Order: $898,128,000$ + +> Presentation: $\langle{ A \mid R}\rangle$ + +On this page, we provide links to verifications that the maximal subgroups of +the McLaughlin group McL define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: + diff --git a/docs/examples/atlas/mathieu/m11.md b/docs/examples/atlas/mathieu/m11.md new file mode 100644 index 0000000..ff62be0 --- /dev/null +++ b/docs/examples/atlas/mathieu/m11.md @@ -0,0 +1,94 @@ +# Mathieu group M~11~ + +> Order: $7,920$ + +> Presentation: $\langle{ a, b \mid a^2 = b^4 = (ab)^{11} = (ab^2)^6 = ababab^{−1}abab^2ab^{−1}abab^{−1}ab^{−1} = 1 }\rangle$ + +On this page, we verify that the above claimed presentation of the Mathieu group +M~11~ defines a group of order $7,920$. + +## The code + +In [libsemigroups_pybind11][], the following script constructs the presentation +for M~11~ and runs the Todd-Coxeter algorithm. + +```python +from libsemigroups_pybind11 import Presentation, ToddCoxeter, congruence_kind, presentation +from libsemigroups_pybind11.words import parse_relations + +# Setup the presentation object with the empty and inverses, so it can represent a group +p = Presentation("abAB") +p.contains_empty_word(True) +presentation.add_inverse_rules(p, "ABab") + +# Add the defining relations +presentation.add_rule(p, parse_relations("a^2"), "") +presentation.add_rule(p, parse_relations("b^4"), "") +presentation.add_rule(p, parse_relations("(ab)^11"), "") +presentation.add_rule(p, parse_relations("(ab^2)^6"), "") +presentation.add_rule(p, parse_relations("ababaBabab^2aBabaBaB"), "") + +# Run the Todd-Coxeter algorithm +tc = ToddCoxeter(congruence_kind.twosided, p) +tc.run() + +assert tc.number_of_classes() == 7920 + +``` + +## The output + +Running the above script produces the following output: + +``` +++++++++++++++++++++++++++++++++ +#0: ToddCoxeter: running for approx. 10.000s +++++++++++++++++++++++++++++++++ +#0: ToddCoxeter: RUN 0 START (strategy() = hlt) +#0: ToddCoxeter: |A| = 4, |R| = 9, |u| + |v| ∈ [2, 22], ∑(|u| + |v|) = 73 +++++++++++++++++++++++++++++++++ +#0: ToddCoxeter: HLT 0.0 START +#0: ToddCoxeter: HLT 0.0.0 | active | killed | defined +#0: ToddCoxeter: nodes | 1 | 0 | 1 +#0: ToddCoxeter: | active | missing | % complete +#0: ToddCoxeter: edges | 0 | 4 | 0.0% +#0: ToddCoxeter: time | run 0 = 19µs | all runs = 19µs | elapsed = 641µs +++++++++++++++++++++++++++++++++ +#0: ToddCoxeter: HLT 0.0 STOP +#0: ToddCoxeter: HLT 0.0.1 | active | killed | defined +#0: ToddCoxeter: nodes | 7,920 | 1,992,427 | 2,000,347 +#0: ToddCoxeter: diff 0.0.0 | +7,919 | +1,992,427 | +2,000,346 +#0: ToddCoxeter: | active | missing | % complete +#0: ToddCoxeter: edges | 31,680 | 0 | 100.0% +#0: ToddCoxeter: diff 0.0.0 | +31,680 | -4 | +100.0% +#0: ToddCoxeter: phase 0.0 = 209ms | run 0 = 209ms | all runs = 209ms | elapsed = 210ms +++++++++++++++++++++++++++++++++ +#0: ToddCoxeter: HLT 0.1.2 | active | killed | defined +#0: ToddCoxeter: nodes | 7,920 | 1,992,427 | 2,000,347 +#0: ToddCoxeter: diff 0.1.1 | +0 | +0 | +0 +#0: ToddCoxeter: diff 0.1.0 | +7,919 | +1,992,427 | +2,000,346 +#0: ToddCoxeter: | active | missing | % complete +#0: ToddCoxeter: edges | 31,680 | 0 | 100.0% +#0: ToddCoxeter: diff 0.1.1 | +0 | +0 | +0.0% +#0: ToddCoxeter: diff 0.1.0 | +31,680 | -4 | +100.0% +#0: ToddCoxeter: phase 0.1 = 209ms | run 0 = 209ms | all runs = 209ms | elapsed = 210ms +++++++++++++++++++++++++++++++++ +#0: ToddCoxeter: RUN 0 STOP (finished) +#0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch +#0: ToddCoxeter: num. phases | 0 | 0 | 1 | 0 +#0: ToddCoxeter: time spent in phases | - (0%) | - (0%) | 209ms (100%) | - (0%) +#0: ToddCoxeter: phase 0.1 = 209ms | run 0 = 209ms | all runs = 209ms | elapsed = 210ms +``` + +:simple-ticktick: The computed size of the group matches the size of the group +provided on [the ATLAS][atlas]: $7,920$. + +!!! note + + The output you see when you run the script yourself might be different from + the above; the numbers produced and time taken will depend on the machine + you are using. However, the size of the group that is reported should be + the same as above. + +[atlas]: https://brauer.maths.qmul.ac.uk/Atlas/v3/spor/ +[libsemigroups_pybind11]: https://libsemigroups.github.io/libsemigroups_pybind11/index.html diff --git a/docs/examples/atlas/mathieu/m12.md b/docs/examples/atlas/mathieu/m12.md new file mode 100644 index 0000000..9868ad0 --- /dev/null +++ b/docs/examples/atlas/mathieu/m12.md @@ -0,0 +1,142 @@ +# Mathieu group M~12~ + +> Order: $95,040$ + +> Presentation: $\langle{ a, b \mid a^2 = b^3 = (ab)^{11} = [a, b]^6 = (ababab^{−1})^6 = 1 }\rangle$ + +On this page, we verify that the above claimed presentation of the Mathieu group +M~12~ defines a group of order $95,040$. + +## The code + +In [libsemigroups_pybind11][], the following script constructs the presentation +for M~12~ and runs the Todd-Coxeter algorithm. + +```python +from libsemigroups_pybind11 import Presentation, ToddCoxeter, congruence_kind, presentation +from libsemigroups_pybind11.words import parse_relations + +# Setup the presentation object with the empty and inverses, so it can represent a group +p = Presentation("abAB") +p.contains_empty_word(True) +presentation.add_inverse_rules(p, "ABab") + +# Add the defining relations +presentation.add_rule(p, parse_relations("a^2"), "") +presentation.add_rule(p, parse_relations("b^3"), "") +presentation.add_rule(p, parse_relations("(ab)^11"), "") +presentation.add_rule(p, parse_relations("(a,b)^6"), "") +presentation.add_rule(p, parse_relations("(ababaB)^6"), "") + + +# Run the Todd-Coxeter algorithm +tc = ToddCoxeter(congruence_kind.twosided, p) +tc.run_for() + +assert tc.number_of_classes() == 95040 +``` + +## The output + +Running the above script produces the following output: + +??? info "Output from the Python script" + + ``` + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: running for approx. 10.000s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 START (strategy() = hlt) + #0: ToddCoxeter: |A| = 4, |R| = 9, |u| + |v| ∈ [2, 36], ∑(|u| + |v|) = 95 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 START + #0: ToddCoxeter: HLT 0.0.0 | active | killed | defined + #0: ToddCoxeter: nodes | 1 | 0 | 1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 0 | 4 | 0.0% + #0: ToddCoxeter: time | run 0 = 21µs | all runs = 21µs | elapsed = 103µs + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 STOP + #0: ToddCoxeter: HLT 0.0.1 | active | killed | defined + #0: ToddCoxeter: nodes | 5,000,004 | 2,964,327 | 7,964,331 + #0: ToddCoxeter: diff 0.0.0 | +5,000,003 | +2,964,327 | +7,964,330 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 5,782,533 | 14,217,483 | 28.9% + #0: ToddCoxeter: diff 0.0.0 | +5,782,533 | +14,217,479 | +28.9% + #0: ToddCoxeter: phase 0.0 = 624ms | run 0 = 624ms | all runs = 624ms | elapsed = 624ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.1 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.1.0 | active | killed | defined + #0: ToddCoxeter: nodes | 5,000,004 | 2,964,327 | 7,964,331 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 5,782,533 | 14,217,483 | 28.9% + #0: ToddCoxeter: time | run 0 = 624ms | all runs = 624ms | elapsed = 624ms + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 5,000,004 + #0: ToddCoxeter: n = lookahead_next() = 5,000,000 + #0: ToddCoxeter: large collapse, number of coincidences 100,002 >= 100,000 = large_collapse()! + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.1.1 | active | killed | defined + #1: ToddCoxeter: nodes | 1,909,907 | 6,057,700 | 7,964,331 + #1: ToddCoxeter: diff 0.1.0 | -3,090,097 | +3,093,373 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 0 | 7,639,628 | 0.0% + #1: ToddCoxeter: diff 0.1.0 | -5,782,533 | -6,577,855 | -28.9% + #1: ToddCoxeter: phase 0.1 = 375ms | run 0 = 1.001s | all runs = 1.001s | elapsed = 1.001s + #1: ToddCoxeter: lookahead progress | ~32.6% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.1 STOP + #0: ToddCoxeter: LOOKAHEAD 0.1.2 | active | killed | defined + #0: ToddCoxeter: nodes | 95,046 | 7,869,285 | 7,964,331 + #0: ToddCoxeter: diff 0.1.1 | -1,814,861 | +1,811,585 | +0 + #0: ToddCoxeter: diff 0.1.0 | -4,904,958 | +4,904,958 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,177 | 7 | 100.0% + #0: ToddCoxeter: diff 0.1.1 | +380,177 | -7,639,621 | +100.0% + #0: ToddCoxeter: diff 0.1.0 | -5,402,356 | -14,217,476 | +71.1% + #0: ToddCoxeter: phase 0.1 = 491ms | run 0 = 1.116s | all runs = 1.116s | elapsed = 1.116s + #0: ToddCoxeter: lookahead_next() is now max(f x a = 190,092, m = 10,000) (-4,809,908) + #0: ToddCoxeter: because f x a < n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 95,046 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: m = lookahead_min() = 10,000 + #0: ToddCoxeter: n = lookahead_next() = 5,000,000 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.2 START + #0: ToddCoxeter: HLT 0.2.0 | active | killed | defined + #0: ToddCoxeter: nodes | 95,046 | 7,869,285 | 7,964,331 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,177 | 7 | 100.0% + #0: ToddCoxeter: time | run 0 = 1.116s | all runs = 1.116s | elapsed = 1.116s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.2 STOP + #0: ToddCoxeter: HLT 0.2.1 | active | killed | defined + #0: ToddCoxeter: nodes | 95,040 | 7,869,292 | 7,964,332 + #0: ToddCoxeter: diff 0.2.0 | -6 | +7 | +1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,160 | 0 | 100.0% + #0: ToddCoxeter: diff 0.2.0 | -17 | -7 | +0.0% + #0: ToddCoxeter: phase 0.2 = 19ms | run 0 = 1.136s | all runs = 1.136s | elapsed = 1.136s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.3.2 | active | killed | defined + #0: ToddCoxeter: nodes | 95,040 | 7,869,292 | 7,964,332 + #0: ToddCoxeter: diff 0.3.1 | +0 | +0 | +0 + #0: ToddCoxeter: diff 0.3.0 | -6 | +7 | +1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,160 | 0 | 100.0% + #0: ToddCoxeter: diff 0.3.1 | +0 | +0 | +0.0% + #0: ToddCoxeter: diff 0.3.0 | -17 | -7 | +0.0% + #0: ToddCoxeter: phase 0.3 = 19ms | run 0 = 1.136s | all runs = 1.136s | elapsed = 1.136s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 STOP (finished) + #0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch + #0: ToddCoxeter: num. phases | 1 | 0 | 2 | 0 + #0: ToddCoxeter: time spent in phases | 491ms (43%) | - (0%) | 644ms (57%) | - (0%) + #0: ToddCoxeter: phase 0.3 = 20ms | run 0 = 1.137s | all runs = 1.137s | elapsed = 1.137s + ``` + +:simple-ticktick: The computed size of the group matches the size of the group +provided on [the ATLAS][atlas]: $95,040$. + +[atlas]: https://brauer.maths.qmul.ac.uk/Atlas/v3/spor/ +[libsemigroups_pybind11]: https://libsemigroups.github.io/libsemigroups_pybind11/index.html diff --git a/docs/examples/atlas/mathieu/m22.md b/docs/examples/atlas/mathieu/m22.md new file mode 100644 index 0000000..f32d718 --- /dev/null +++ b/docs/examples/atlas/mathieu/m22.md @@ -0,0 +1,565 @@ +# Mathieu group M~22~ + +> Order: $443,520$ + +> Presentation: $\langle{ a, b \mid a^2 = b^4 = (ab)^{11} = (ab^2)^5 = [a,bab]^3 = (ababab^{−1})^5 = 1 }\rangle$ + +On this page, we verify that the above claimed presentation of the Mathieu group +M~22~ defines a group of order $443,520$. + +## The code + +In [libsemigroups_pybind11][], the following script constructs the presentation +for M~11~ and runs the Todd-Coxeter algorithm. + +```python +from libsemigroups_pybind11 import Presentation, ToddCoxeter, congruence_kind, presentation +from libsemigroups_pybind11.words import parse_relations + +# Setup the presentation object with the empty and inverses, so it can represent a group +p = Presentation("abAB") +p.contains_empty_word(True) +presentation.add_inverse_rules(p, "ABab") + +# Add the defining relations +presentation.add_rule(p, parse_relations("a^2"), "") +presentation.add_rule(p, parse_relations("b^4"), "") +presentation.add_rule(p, parse_relations("(ab)^11"), "") +presentation.add_rule(p, parse_relations("(ab^2)^5"), "") +presentation.add_rule(p, parse_relations("(a,bab)^3"), "") +presentation.add_rule(p, parse_relations("(ababaB)^5"), "") + + +# Run the Todd-Coxeter algorithm +tc = ToddCoxeter(congruence_kind.twosided, p) +tc.run() + +assert tc.number_of_classes() == 443520 +``` + +## The output + +Running the above script produces the following output: + +??? info "Output from the Python script" + + ``` + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: running for approx. 30.000s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 START (strategy() = hlt) + #0: ToddCoxeter: |A| = 4, |R| = 10, |u| + |v| ∈ [2, 30], ∑(|u| + |v|) = 105 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 START + #0: ToddCoxeter: HLT 0.0.0 | active | killed | defined + #0: ToddCoxeter: nodes | 1 | 0 | 1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 0 | 4 | 0.0% + #0: ToddCoxeter: time | run 0 = 19µs | all runs = 19µs | elapsed = 89µs + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 STOP + #0: ToddCoxeter: HLT 0.0.1 | active | killed | defined + #0: ToddCoxeter: nodes | 5,000,018 | 1,632,158 | 6,632,176 + #0: ToddCoxeter: diff 0.0.0 | +5,000,017 | +1,632,158 | +6,632,175 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 5,679,076 | 14,320,996 | 28.4% + #0: ToddCoxeter: diff 0.0.0 | +5,679,076 | +14,320,992 | +28.4% + #0: ToddCoxeter: phase 0.0 = 547ms | run 0 = 547ms | all runs = 547ms | elapsed = 547ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.1 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.1.0 | active | killed | defined + #0: ToddCoxeter: nodes | 5,000,018 | 1,632,158 | 6,632,176 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 5,679,076 | 14,320,996 | 28.4% + #0: ToddCoxeter: time | run 0 = 547ms | all runs = 547ms | elapsed = 547ms + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 5,000,018 + #0: ToddCoxeter: n = lookahead_next() = 5,000,000 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.1.1 | active | killed | defined + #1: ToddCoxeter: nodes | 2,644,921 | 3,987,547 | 6,632,176 + #1: ToddCoxeter: diff 0.1.0 | -2,355,097 | +2,355,389 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 7,553,691 | 3,025,993 | 71.4% + #1: ToddCoxeter: diff 0.1.0 | +1,874,615 | -11,295,003 | +43.0% + #1: ToddCoxeter: phase 0.1 = 452ms | run 0 = 1.000s | all runs = 1.000s | elapsed = 1.001s + #1: ToddCoxeter: lookahead progress | ~60.5% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.1 STOP + #0: ToddCoxeter: LOOKAHEAD 0.1.2 | active | killed | defined + #0: ToddCoxeter: nodes | 2,423,713 | 4,208,463 | 6,632,176 + #0: ToddCoxeter: diff 0.1.1 | -221,208 | +220,916 | +0 + #0: ToddCoxeter: diff 0.1.0 | -2,576,305 | +2,576,305 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 7,815,443 | 1,879,409 | 80.6% + #0: ToddCoxeter: diff 0.1.1 | +261,752 | -1,146,584 | +9.2% + #0: ToddCoxeter: diff 0.1.0 | +2,136,367 | -12,441,587 | +52.2% + #0: ToddCoxeter: phase 0.1 = 500ms | run 0 = 1.049s | all runs = 1.049s | elapsed = 1.049s + #0: ToddCoxeter: lookahead_next() is now max(f x a = 4,847,426, m = 10,000) (-152,574) + #0: ToddCoxeter: because f x a < n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 2,423,713 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: m = lookahead_min() = 10,000 + #0: ToddCoxeter: n = lookahead_next() = 5,000,000 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.2 START + #0: ToddCoxeter: HLT 0.2.0 | active | killed | defined + #0: ToddCoxeter: nodes | 2,423,713 | 4,208,463 | 6,632,176 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 7,815,443 | 1,879,409 | 80.6% + #0: ToddCoxeter: time | run 0 = 1.049s | all runs = 1.049s | elapsed = 1.049s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.2 STOP + #0: ToddCoxeter: HLT 0.2.1 | active | killed | defined + #0: ToddCoxeter: nodes | 4,847,474 | 4,320,458 | 9,167,932 + #0: ToddCoxeter: diff 0.2.0 | +2,423,761 | +111,995 | +2,535,756 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 10,422,837 | 8,967,059 | 53.8% + #0: ToddCoxeter: diff 0.2.0 | +2,607,394 | +7,087,650 | -26.9% + #0: ToddCoxeter: phase 0.2 = 89ms | run 0 = 1.138s | all runs = 1.138s | elapsed = 1.138s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.3 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.3.0 | active | killed | defined + #0: ToddCoxeter: nodes | 4,847,474 | 4,320,458 | 9,167,932 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 10,422,837 | 8,967,059 | 53.8% + #0: ToddCoxeter: time | run 0 = 1.138s | all runs = 1.138s | elapsed = 1.138s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,847,474 + #0: ToddCoxeter: n = lookahead_next() = 4,847,426 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.3 STOP + #0: ToddCoxeter: LOOKAHEAD 0.3.1 | active | killed | defined + #0: ToddCoxeter: nodes | 3,512,400 | 5,655,532 | 9,167,932 + #0: ToddCoxeter: diff 0.3.0 | -1,335,074 | +1,335,074 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 11,491,787 | 2,557,813 | 81.8% + #0: ToddCoxeter: diff 0.3.0 | +1,068,950 | -6,409,246 | +28.0% + #0: ToddCoxeter: phase 0.3 = 718ms | run 0 = 1.856s | all runs = 1.856s | elapsed = 1.857s + #0: ToddCoxeter: lookahead_next() is now 4,847,426 (+0) + #0: ToddCoxeter: because: + #0: ToddCoxeter: 1. n <= f x a = 7,024,800 + #0: ToddCoxeter: 2. a <= n + #0: ToddCoxeter: 3. l >= (l + a) / t = 1,211,868 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 3,512,400 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 1,335,074 + #0: ToddCoxeter: n = lookahead_next() = 4,847,426 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.4 START + #0: ToddCoxeter: HLT 0.4.0 | active | killed | defined + #0: ToddCoxeter: nodes | 3,512,400 | 5,655,532 | 9,167,932 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 11,491,787 | 2,557,813 | 81.8% + #0: ToddCoxeter: time | run 0 = 1.857s | all runs = 1.857s | elapsed = 1.857s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.4 STOP + #0: ToddCoxeter: HLT 0.4.1 | active | killed | defined + #0: ToddCoxeter: nodes | 4,847,449 | 5,703,629 | 10,551,078 + #0: ToddCoxeter: diff 0.4.0 | +1,335,049 | +48,097 | +1,383,146 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 12,934,269 | 6,455,527 | 66.7% + #0: ToddCoxeter: diff 0.4.0 | +1,442,482 | +3,897,714 | -15.1% + #0: ToddCoxeter: phase 0.4 = 67ms | run 0 = 1.924s | all runs = 1.924s | elapsed = 1.924s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.5 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.5.0 | active | killed | defined + #0: ToddCoxeter: nodes | 4,847,449 | 5,703,629 | 10,551,078 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 12,934,269 | 6,455,527 | 66.7% + #0: ToddCoxeter: time | run 0 = 1.924s | all runs = 1.924s | elapsed = 1.924s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,847,449 + #0: ToddCoxeter: n = lookahead_next() = 4,847,426 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.5.1 | active | killed | defined + #1: ToddCoxeter: nodes | 4,820,487 | 5,730,591 | 10,551,078 + #1: ToddCoxeter: diff 0.5.0 | -26,962 | +26,962 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 12,908,450 | 6,373,498 | 66.9% + #1: ToddCoxeter: diff 0.5.0 | -25,819 | -82,029 | +0.2% + #1: ToddCoxeter: phase 0.5 = 77ms | run 0 = 2.001s | all runs = 2.001s | elapsed = 2.001s + #1: ToddCoxeter: lookahead progress | ~11.0% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.5 STOP + #0: ToddCoxeter: LOOKAHEAD 0.5.2 | active | killed | defined + #0: ToddCoxeter: nodes | 4,134,106 | 6,416,972 | 10,551,078 + #0: ToddCoxeter: diff 0.5.1 | -686,381 | +686,381 | +0 + #0: ToddCoxeter: diff 0.5.0 | -713,343 | +713,343 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 13,557,552 | 2,978,872 | 82.0% + #0: ToddCoxeter: diff 0.5.1 | +649,102 | -3,394,626 | +15.0% + #0: ToddCoxeter: diff 0.5.0 | +623,283 | -3,476,655 | +15.3% + #0: ToddCoxeter: phase 0.5 = 856ms | run 0 = 2.780s | all runs = 2.780s | elapsed = 2.780s + #0: ToddCoxeter: lookahead_next() is now n x f = 9,694,852 (+4,847,426) + #0: ToddCoxeter: because: l < (l + a) / t = 1,211,862 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,134,106 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 713,343 + #0: ToddCoxeter: n = lookahead_next() = 4,847,426 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.6 START + #0: ToddCoxeter: HLT 0.6.0 | active | killed | defined + #0: ToddCoxeter: nodes | 4,134,106 | 6,416,972 | 10,551,078 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 13,557,552 | 2,978,872 | 82.0% + #0: ToddCoxeter: time | run 0 = 2.780s | all runs = 2.780s | elapsed = 2.780s + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: HLT 0.6.1 | active | killed | defined + #1: ToddCoxeter: nodes | 8,388,608 | 6,594,998 | 14,983,606 + #1: ToddCoxeter: diff 0.6.0 | +4,254,502 | +178,026 | +4,432,528 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 18,160,579 | 15,393,853 | 54.1% + #1: ToddCoxeter: diff 0.6.0 | +4,603,027 | +12,414,981 | -27.9% + #1: ToddCoxeter: phase 0.6 = 221ms | run 0 = 3.001s | all runs = 3.001s | elapsed = 3.001s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.6 STOP + #0: ToddCoxeter: HLT 0.6.2 | active | killed | defined + #0: ToddCoxeter: nodes | 9,694,873 | 6,657,105 | 16,351,978 + #0: ToddCoxeter: diff 0.6.1 | +1,306,265 | +62,107 | +1,368,372 + #0: ToddCoxeter: diff 0.6.0 | +5,560,767 | +240,133 | +5,800,900 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 19,575,370 | 19,204,122 | 50.5% + #0: ToddCoxeter: diff 0.6.1 | +1,414,791 | +3,810,269 | -3.6% + #0: ToddCoxeter: diff 0.6.0 | +6,017,818 | +16,225,250 | -31.5% + #0: ToddCoxeter: phase 0.6 = 520ms | run 0 = 3.301s | all runs = 3.301s | elapsed = 3.301s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.7 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.7.0 | active | killed | defined + #0: ToddCoxeter: nodes | 9,694,873 | 6,657,105 | 16,351,978 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 19,575,370 | 19,204,122 | 50.5% + #0: ToddCoxeter: time | run 0 = 3.301s | all runs = 3.301s | elapsed = 3.301s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 9,694,873 + #0: ToddCoxeter: n = lookahead_next() = 9,694,852 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.7.1 | active | killed | defined + #1: ToddCoxeter: nodes | 9,431,978 | 6,920,002 | 16,351,978 + #1: ToddCoxeter: diff 0.7.0 | -262,895 | +262,897 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 19,360,399 | 18,367,513 | 51.3% + #1: ToddCoxeter: diff 0.7.0 | -214,971 | -836,609 | +0.8% + #1: ToddCoxeter: phase 0.7 = 700ms | run 0 = 4.001s | all runs = 4.001s | elapsed = 4.001s + #1: ToddCoxeter: lookahead progress | ~41.5% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.7 STOP + #0: ToddCoxeter: LOOKAHEAD 0.7.2 | active | killed | defined + #0: ToddCoxeter: nodes | 6,784,030 | 9,567,948 | 16,351,978 + #0: ToddCoxeter: diff 0.7.1 | -2,647,948 | +2,647,946 | +0 + #0: ToddCoxeter: diff 0.7.0 | -2,910,843 | +2,910,843 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 22,154,799 | 4,981,321 | 81.6% + #0: ToddCoxeter: diff 0.7.1 | +2,794,400 | -13,386,192 | +30.3% + #0: ToddCoxeter: diff 0.7.0 | +2,579,429 | -14,222,801 | +31.2% + #0: ToddCoxeter: phase 0.7 = 1.445s | run 0 = 4.746s | all runs = 4.746s | elapsed = 4.746s + #0: ToddCoxeter: lookahead_next() is now 9,694,852 (+0) + #0: ToddCoxeter: because: + #0: ToddCoxeter: 1. n <= f x a = 13,568,060 + #0: ToddCoxeter: 2. a <= n + #0: ToddCoxeter: 3. l >= (l + a) / t = 2,423,718 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 6,784,030 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 2,910,843 + #0: ToddCoxeter: n = lookahead_next() = 9,694,852 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.8 START + #0: ToddCoxeter: HLT 0.8.0 | active | killed | defined + #0: ToddCoxeter: nodes | 6,784,030 | 9,567,948 | 16,351,978 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 22,154,799 | 4,981,321 | 81.6% + #0: ToddCoxeter: time | run 0 = 4.746s | all runs = 4.746s | elapsed = 4.746s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.8 STOP + #0: ToddCoxeter: HLT 0.8.1 | active | killed | defined + #0: ToddCoxeter: nodes | 9,694,854 | 9,675,719 | 19,370,573 + #0: ToddCoxeter: diff 0.8.0 | +2,910,824 | +107,771 | +3,018,595 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 25,297,258 | 13,482,158 | 65.2% + #0: ToddCoxeter: diff 0.8.0 | +3,142,459 | +8,500,837 | -16.4% + #0: ToddCoxeter: phase 0.8 = 130ms | run 0 = 4.876s | all runs = 4.876s | elapsed = 4.876s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.9 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.9.0 | active | killed | defined + #0: ToddCoxeter: nodes | 9,694,854 | 9,675,719 | 19,370,573 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 25,297,258 | 13,482,158 | 65.2% + #0: ToddCoxeter: time | run 0 = 4.876s | all runs = 4.876s | elapsed = 4.876s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 9,694,854 + #0: ToddCoxeter: n = lookahead_next() = 9,694,852 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.9.1 | active | killed | defined + #1: ToddCoxeter: nodes | 9,648,811 | 9,721,762 | 19,370,573 + #1: ToddCoxeter: diff 0.9.0 | -46,043 | +46,043 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 25,256,260 | 13,338,984 | 65.4% + #1: ToddCoxeter: diff 0.9.0 | -40,998 | -143,174 | +0.2% + #1: ToddCoxeter: phase 0.9 = 125ms | run 0 = 5.001s | all runs = 5.001s | elapsed = 5.002s + #1: ToddCoxeter: lookahead progress | ~9.5% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.9.2 | active | killed | defined + #1: ToddCoxeter: nodes | 9,403,427 | 9,967,160 | 19,370,573 + #1: ToddCoxeter: diff 0.9.1 | -245,384 | +245,398 | +0 + #1: ToddCoxeter: diff 0.9.0 | -291,427 | +291,441 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 25,010,253 | 12,603,455 | 66.5% + #1: ToddCoxeter: diff 0.9.1 | -246,007 | -735,529 | +1.1% + #1: ToddCoxeter: diff 0.9.0 | -287,005 | -878,703 | +1.3% + #1: ToddCoxeter: phase 0.9 = 1.126s | run 0 = 6.002s | all runs = 6.002s | elapsed = 6.002s + #1: ToddCoxeter: lookahead progress | ~63.4% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.9 STOP + #0: ToddCoxeter: LOOKAHEAD 0.9.3 | active | killed | defined + #0: ToddCoxeter: nodes | 8,086,523 | 11,284,050 | 19,370,573 + #0: ToddCoxeter: diff 0.9.2 | -1,316,904 | +1,316,890 | +0 + #0: ToddCoxeter: diff 0.9.0 | -1,608,331 | +1,608,331 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 26,555,088 | 5,791,004 | 82.1% + #0: ToddCoxeter: diff 0.9.2 | +1,544,835 | -6,812,451 | +15.6% + #0: ToddCoxeter: diff 0.9.0 | +1,257,830 | -7,691,154 | +16.9% + #0: ToddCoxeter: phase 0.9 = 1.690s | run 0 = 6.566s | all runs = 6.566s | elapsed = 6.566s + #0: ToddCoxeter: lookahead_next() is now n x f = 19,389,704 (+9,694,852) + #0: ToddCoxeter: because: l < (l + a) / t = 2,423,713 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 8,086,523 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 1,608,331 + #0: ToddCoxeter: n = lookahead_next() = 9,694,852 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.10 START + #0: ToddCoxeter: HLT 0.10.0 | active | killed | defined + #0: ToddCoxeter: nodes | 8,086,523 | 11,284,050 | 19,370,573 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 26,555,088 | 5,791,004 | 82.1% + #0: ToddCoxeter: time | run 0 = 6.566s | all runs = 6.566s | elapsed = 6.566s + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: HLT 0.10.1 | active | killed | defined + #1: ToddCoxeter: nodes | 16,777,216 | 11,642,699 | 28,419,915 + #1: ToddCoxeter: diff 0.10.0 | +8,690,693 | +358,649 | +9,049,342 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 35,954,563 | 31,154,301 | 53.6% + #1: ToddCoxeter: diff 0.10.0 | +9,399,475 | +25,363,297 | -28.5% + #1: ToddCoxeter: phase 0.10 = 436ms | run 0 = 7.002s | all runs = 7.002s | elapsed = 7.002s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.10 STOP + #0: ToddCoxeter: HLT 0.10.2 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,750 | 11,773,835 | 31,163,585 + #0: ToddCoxeter: diff 0.10.1 | +2,612,534 | +131,136 | +2,743,670 + #0: ToddCoxeter: diff 0.10.0 | +11,303,227 | +489,785 | +11,793,012 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 38,786,740 | 38,772,260 | 50.0% + #0: ToddCoxeter: diff 0.10.1 | +2,832,177 | +7,617,959 | -3.6% + #0: ToddCoxeter: diff 0.10.0 | +12,231,652 | +32,981,256 | -32.1% + #0: ToddCoxeter: phase 0.10 = 1.051s | run 0 = 7.617s | all runs = 7.617s | elapsed = 7.617s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.11 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.11.0 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,750 | 11,773,835 | 31,163,585 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 38,786,740 | 38,772,260 | 50.0% + #0: ToddCoxeter: time | run 0 = 7.617s | all runs = 7.617s | elapsed = 7.617s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 19,389,750 + #0: ToddCoxeter: n = lookahead_next() = 19,389,704 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.11.1 | active | killed | defined + #1: ToddCoxeter: nodes | 19,119,246 | 12,044,357 | 31,163,585 + #1: ToddCoxeter: diff 0.11.0 | -270,504 | +270,522 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 38,564,145 | 37,912,839 | 50.4% + #1: ToddCoxeter: diff 0.11.0 | -222,595 | -859,421 | +0.4% + #1: ToddCoxeter: phase 0.11 = 385ms | run 0 = 8.002s | all runs = 8.002s | elapsed = 8.002s + #1: ToddCoxeter: lookahead progress | ~12.6% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.11.2 | active | killed | defined + #1: ToddCoxeter: nodes | 18,894,507 | 12,269,078 | 31,163,585 + #1: ToddCoxeter: diff 0.11.1 | -224,739 | +224,721 | +0 + #1: ToddCoxeter: diff 0.11.0 | -495,243 | +495,243 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 38,371,598 | 37,206,430 | 50.8% + #1: ToddCoxeter: diff 0.11.1 | -192,547 | -706,409 | +0.3% + #1: ToddCoxeter: diff 0.11.0 | -415,142 | -1,565,830 | +0.8% + #1: ToddCoxeter: phase 0.11 = 1.385s | run 0 = 9.003s | all runs = 9.003s | elapsed = 9.003s + #1: ToddCoxeter: lookahead progress | ~38.8% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.11.3 | active | killed | defined + #1: ToddCoxeter: nodes | 15,851,580 | 15,312,085 | 31,163,585 + #1: ToddCoxeter: diff 0.11.2 | -3,042,927 | +3,043,007 | +0 + #1: ToddCoxeter: diff 0.11.0 | -3,538,170 | +3,538,250 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 41,333,919 | 22,072,401 | 65.2% + #1: ToddCoxeter: diff 0.11.2 | +2,962,321 | -15,134,029 | +14.4% + #1: ToddCoxeter: diff 0.11.0 | +2,547,179 | -16,699,859 | +15.2% + #1: ToddCoxeter: phase 0.11 = 2.386s | run 0 = 10.003s | all runs = 10.003s | elapsed = 10.003s + #1: ToddCoxeter: lookahead progress | ~62.6% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.11 STOP + #0: ToddCoxeter: LOOKAHEAD 0.11.4 | active | killed | defined + #0: ToddCoxeter: nodes | 13,427,510 | 17,736,075 | 31,163,585 + #0: ToddCoxeter: diff 0.11.3 | -2,424,070 | +2,423,990 | +0 + #0: ToddCoxeter: diff 0.11.0 | -5,962,240 | +5,962,240 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 43,882,513 | 9,827,527 | 81.7% + #0: ToddCoxeter: diff 0.11.3 | +2,548,594 | -12,244,874 | +16.5% + #0: ToddCoxeter: diff 0.11.0 | +5,095,773 | -28,944,733 | +31.7% + #0: ToddCoxeter: phase 0.11 = 2.893s | run 0 = 10.511s | all runs = 10.511s | elapsed = 10.511s + #0: ToddCoxeter: lookahead_next() is now 19,389,704 (+0) + #0: ToddCoxeter: because: + #0: ToddCoxeter: 1. n <= f x a = 26,855,020 + #0: ToddCoxeter: 2. a <= n + #0: ToddCoxeter: 3. l >= (l + a) / t = 4,847,437 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 13,427,510 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 5,962,240 + #0: ToddCoxeter: n = lookahead_next() = 19,389,704 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.12 START + #0: ToddCoxeter: HLT 0.12.0 | active | killed | defined + #0: ToddCoxeter: nodes | 13,427,510 | 17,736,075 | 31,163,585 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 43,882,513 | 9,827,527 | 81.7% + #0: ToddCoxeter: time | run 0 = 10.511s | all runs = 10.511s | elapsed = 10.511s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.12 STOP + #0: ToddCoxeter: HLT 0.12.1 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,776 | 17,959,888 | 37,349,664 + #0: ToddCoxeter: diff 0.12.0 | +5,962,266 | +223,813 | +6,186,079 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 50,324,580 | 27,234,524 | 64.9% + #0: ToddCoxeter: diff 0.12.0 | +6,442,067 | +17,406,997 | -16.8% + #0: ToddCoxeter: phase 0.12 = 267ms | run 0 = 10.778s | all runs = 10.778s | elapsed = 10.779s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.13 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.13.0 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,776 | 17,959,888 | 37,349,664 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 50,324,580 | 27,234,524 | 64.9% + #0: ToddCoxeter: time | run 0 = 10.778s | all runs = 10.778s | elapsed = 10.779s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 19,389,776 + #0: ToddCoxeter: n = lookahead_next() = 19,389,704 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.13.1 | active | killed | defined + #1: ToddCoxeter: nodes | 19,314,200 | 18,035,464 | 37,349,664 + #1: ToddCoxeter: diff 0.13.0 | -75,576 | +75,576 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 50,245,486 | 27,011,314 | 65.0% + #1: ToddCoxeter: diff 0.13.0 | -79,094 | -223,210 | +0.2% + #1: ToddCoxeter: phase 0.13 = 224ms | run 0 = 11.003s | all runs = 11.003s | elapsed = 11.003s + #1: ToddCoxeter: lookahead progress | ~9.0% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.13.2 | active | killed | defined + #1: ToddCoxeter: nodes | 19,102,330 | 18,247,350 | 37,349,664 + #1: ToddCoxeter: diff 0.13.1 | -211,870 | +211,886 | +0 + #1: ToddCoxeter: diff 0.13.0 | -287,446 | +287,462 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 50,032,914 | 26,376,406 | 65.5% + #1: ToddCoxeter: diff 0.13.1 | -212,572 | -634,908 | +0.4% + #1: ToddCoxeter: diff 0.13.0 | -291,666 | -858,118 | +0.6% + #1: ToddCoxeter: phase 0.13 = 1.225s | run 0 = 12.003s | all runs = 12.003s | elapsed = 12.003s + #1: ToddCoxeter: lookahead progress | ~31.3% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.13.3 | active | killed | defined + #1: ToddCoxeter: nodes | 18,872,056 | 18,477,610 | 37,349,664 + #1: ToddCoxeter: diff 0.13.2 | -230,274 | +230,260 | +0 + #1: ToddCoxeter: diff 0.13.0 | -517,720 | +517,722 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 49,788,690 | 25,699,534 | 66.0% + #1: ToddCoxeter: diff 0.13.2 | -244,224 | -676,872 | +0.5% + #1: ToddCoxeter: diff 0.13.0 | -535,890 | -1,534,990 | +1.1% + #1: ToddCoxeter: phase 0.13 = 2.225s | run 0 = 13.004s | all runs = 13.004s | elapsed = 13.004s + #1: ToddCoxeter: lookahead progress | ~58.4% + #0: ToddCoxeter: large collapse, number of coincidences 100,000 >= 100,000 = large_collapse()! + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.13.4 | active | killed | defined + #1: ToddCoxeter: nodes | 12,447,893 | 24,901,915 | 37,349,664 + #1: ToddCoxeter: diff 0.13.3 | -6,424,163 | +6,424,305 | +0 + #1: ToddCoxeter: diff 0.13.0 | -6,941,883 | +6,942,027 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 0 | 49,791,572 | 0.0% + #1: ToddCoxeter: diff 0.13.3 | -49,788,690 | +24,092,038 | -66.0% + #1: ToddCoxeter: diff 0.13.0 | -50,324,580 | +22,557,048 | -64.9% + #1: ToddCoxeter: phase 0.13 = 3.225s | run 0 = 14.004s | all runs = 14.004s | elapsed = 14.004s + #1: ToddCoxeter: lookahead progress | ~66.6% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.13.5 | active | killed | defined + #1: ToddCoxeter: nodes | 5,024,869 | 32,324,910 | 37,349,664 + #1: ToddCoxeter: diff 0.13.4 | -7,423,024 | +7,422,995 | +0 + #1: ToddCoxeter: diff 0.13.0 | -14,364,907 | +14,365,022 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 0 | 20,099,476 | 0.0% + #1: ToddCoxeter: diff 0.13.4 | +0 | -29,692,096 | +0.0% + #1: ToddCoxeter: diff 0.13.0 | -50,324,580 | -7,135,048 | -64.9% + #1: ToddCoxeter: phase 0.13 = 4.226s | run 0 = 15.004s | all runs = 15.004s | elapsed = 15.004s + #1: ToddCoxeter: lookahead progress | ~66.6% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.13 STOP + #0: ToddCoxeter: LOOKAHEAD 0.13.6 | active | killed | defined + #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 + #0: ToddCoxeter: diff 0.13.5 | -4,581,349 | +4,581,234 | +0 + #0: ToddCoxeter: diff 0.13.0 | -18,946,256 | +18,946,256 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% + #0: ToddCoxeter: diff 0.13.5 | +1,774,080 | -20,099,476 | +100.0% + #0: ToddCoxeter: diff 0.13.0 | -48,550,500 | -27,234,524 | +35.1% + #0: ToddCoxeter: phase 0.13 = 5.080s | run 0 = 15.858s | all runs = 15.858s | elapsed = 15.858s + #0: ToddCoxeter: lookahead_next() is now max(f x a = 887,040, m = 10,000) (-18,502,664) + #0: ToddCoxeter: because f x a < n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 443,520 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: m = lookahead_min() = 10,000 + #0: ToddCoxeter: n = lookahead_next() = 19,389,704 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.14 START + #0: ToddCoxeter: HLT 0.14.0 | active | killed | defined + #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% + #0: ToddCoxeter: time | run 0 = 15.858s | all runs = 15.858s | elapsed = 15.858s + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: HLT 0.14.1 | active | killed | defined + #1: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 + #1: ToddCoxeter: diff 0.14.0 | +0 | +0 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% + #1: ToddCoxeter: diff 0.14.0 | +0 | +0 | +0.0% + #1: ToddCoxeter: phase 0.14 = 146ms | run 0 = 16.004s | all runs = 16.004s | elapsed = 16.005s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.14 STOP + #0: ToddCoxeter: HLT 0.14.2 | active | killed | defined + #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 + #0: ToddCoxeter: diff 0.14.1 | +0 | +0 | +0 + #0: ToddCoxeter: diff 0.14.0 | +0 | +0 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% + #0: ToddCoxeter: diff 0.14.1 | +0 | +0 | +0.0% + #0: ToddCoxeter: diff 0.14.0 | +0 | +0 | +0.0% + #0: ToddCoxeter: phase 0.14 = 151ms | run 0 = 16.009s | all runs = 16.009s | elapsed = 16.010s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.15.3 | active | killed | defined + #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 + #0: ToddCoxeter: diff 0.15.2 | +0 | +0 | +0 + #0: ToddCoxeter: diff 0.15.0 | +0 | +0 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% + #0: ToddCoxeter: diff 0.15.2 | +0 | +0 | +0.0% + #0: ToddCoxeter: diff 0.15.0 | +0 | +0 | +0.0% + #0: ToddCoxeter: phase 0.15 = 151ms | run 0 = 16.010s | all runs = 16.010s | elapsed = 16.010s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 STOP (finished) + #0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch + #0: ToddCoxeter: num. phases | 7 | 0 | 8 | 0 + #0: ToddCoxeter: time spent in phases | 13.184s (82%) | - (0%) | 2.826s (18%) | - (0%) + #0: ToddCoxeter: phase 0.15 = 160ms | run 0 = 16.019s | all runs = 16.019s | elapsed = 16.019s + ``` + +:simple-ticktick: The computed size of the group matches the size of the group +provided on [the ATLAS][atlas]: $443,520$. + +[atlas]: https://brauer.maths.qmul.ac.uk/Atlas/v3/spor/ +[libsemigroups_pybind11]: https://libsemigroups.github.io/libsemigroups_pybind11/index.html diff --git a/docs/examples/atlas/mathieu/m23/index.md b/docs/examples/atlas/mathieu/m23/index.md new file mode 100644 index 0000000..c732425 --- /dev/null +++ b/docs/examples/atlas/mathieu/m23/index.md @@ -0,0 +1,13 @@ +# Mathieu group M~23~ + +> Order: $10,200,960$ + +> Presentation: $\langle{ A \mid R}\rangle$ + +On this page, we provide links to verifications that the maximal subgroups of +the Mathieu group M~23~ define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: + diff --git a/docs/examples/atlas/mathieu/m24/index.md b/docs/examples/atlas/mathieu/m24/index.md new file mode 100644 index 0000000..0eb51fb --- /dev/null +++ b/docs/examples/atlas/mathieu/m24/index.md @@ -0,0 +1,13 @@ +# Mathieu group M~24~ + +> Order: $244,823,040$ + +> Presentation: $\langle{ A \mid R}\rangle$ + +On this page, we provide links to verifications that the maximal subgroups of +the Mathieu group M~24~ define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: + diff --git a/docs/examples/atlas/misc/t.md b/docs/examples/atlas/misc/t.md new file mode 100644 index 0000000..bf48d5b --- /dev/null +++ b/docs/examples/atlas/misc/t.md @@ -0,0 +1,17 @@ +# Tits group T + +> Order: $17,971,200$ + +> Presentation: $\langle{ A \mid R}\rangle$ + +On this page, we verify that the above claimed presentation of the Tits group T +defines a group of order $17,971,200$. + +## The code + +Coming soon! + +## The output + +Coming soon! + diff --git a/docs/examples/atlas/monster-sections/fi22/index.md b/docs/examples/atlas/monster-sections/fi22/index.md new file mode 100644 index 0000000..4b5681d --- /dev/null +++ b/docs/examples/atlas/monster-sections/fi22/index.md @@ -0,0 +1,13 @@ +# Fischer group Fi~22~ + +> Order: $64,561,751,654,400$ + +> Presentation: $\langle{ A \mid R}\rangle$ + +On this page, we provide links to verifications that the maximal subgroups of +the Fischer group Fi~22~ define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: + diff --git a/docs/examples/atlas/monster-sections/he/index.md b/docs/examples/atlas/monster-sections/he/index.md new file mode 100644 index 0000000..357db23 --- /dev/null +++ b/docs/examples/atlas/monster-sections/he/index.md @@ -0,0 +1,13 @@ +# Held group He + +> Order: $4,030,387,200$ + +> Presentation: $\langle{ A \mid R}\rangle$ + +On this page, we provide links to verifications that the maximal subgroups of +the Held group He define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: + diff --git a/docs/examples/atlas/pariahs/j1.md b/docs/examples/atlas/pariahs/j1.md new file mode 100644 index 0000000..d13a34d --- /dev/null +++ b/docs/examples/atlas/pariahs/j1.md @@ -0,0 +1,16 @@ +# Janko group J~1~ + +> Order: $175,560$ + +> Presentation: $\langle{ A \mid R}\rangle$ + +On this page, we verify that the above claimed presentation of the Janko group +J~1~ defines a group of order $175,560$. + +## The code + +Coming soon! + +## The output + +Coming soon! diff --git a/docs/examples/atlas/pariahs/j3.md b/docs/examples/atlas/pariahs/j3.md new file mode 100644 index 0000000..0dcdca1 --- /dev/null +++ b/docs/examples/atlas/pariahs/j3.md @@ -0,0 +1,16 @@ +# Janko group J~3~ + +> Order: $50,232,960$ + +> Presentation: $\langle{ A \mid R}\rangle$ + +On this page, we verify that the above claimed presentation of the Janko group +J~3~ defines a group of order $50,232,960$. + +## The code + +Coming soon! + +## The output + +Coming soon! diff --git a/docs/examples/atlas/pariahs/j4/index.md b/docs/examples/atlas/pariahs/j4/index.md new file mode 100644 index 0000000..a80fc7f --- /dev/null +++ b/docs/examples/atlas/pariahs/j4/index.md @@ -0,0 +1,13 @@ +# Janko group J~4~ + +> Order: $86,775,571,046,077,562,880$ + +> Presentation: $\langle{ A \mid R}\rangle$ + +On this page, we provide links to verifications that the maximal subgroups of +the Janko group J~4~ define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: + diff --git a/docs/examples/atlas/pariahs/ru/index.md b/docs/examples/atlas/pariahs/ru/index.md new file mode 100644 index 0000000..b47a2b7 --- /dev/null +++ b/docs/examples/atlas/pariahs/ru/index.md @@ -0,0 +1,13 @@ +# Rudvalis group Ru + +> Order: $145,926,144,000$ + +> Presentation: $\langle{ A \mid R}\rangle$ + +On this page, we provide links to verifications that the maximal subgroups of +the Rudvalis group Ru define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: + diff --git a/docs/stylesheets/extra.css b/docs/stylesheets/extra.css new file mode 100644 index 0000000..8f73613 --- /dev/null +++ b/docs/stylesheets/extra.css @@ -0,0 +1,47 @@ +/* .atlas-summary { + text-align: center; +} */ + +.column { + float: left; + width: 50%; +} + +/* Clear floats after the columns */ +.row:after { + content: ""; + display: table; + clear: both; +} + +.atlas-summary table:not([class]) { + th:not([align]), + td:not([align]) { + text-align: center; /* Reset alignment for table cells */ + } +} + +.atlas-summary a { + color: #000000; + text-decoration: none; +} + +.correct-size { + background-color: #4dac26; +} + +.correct-index { + background-color: #b8e186; +} + +.incorrect-size { + background-color: #f1b6da; +} + +.could-not-verify { + background-color: #cccccc; +} + +.no-presentation { + background-color: grey; +} diff --git a/mkdocs.yml b/mkdocs.yml index a802fc4..fd19a6f 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -16,9 +16,40 @@ nav: - "Python: Semigroups defined by generators": py/generated.md - "Python: Finitely presented semigroups": py/fp.md - "Python: Worksheet": py/worksheet.md - - Case studies: - - case-studies/index.md - - case-studies/short.md + - Examples: + - examples/index.md + - examples/short.md + - "Verifying presentations in the ATLAS of Finite Groups": + - examples/atlas/index.md + - "Mathieu groups": + - examples/atlas/mathieu/m11.md + - examples/atlas/mathieu/m12.md + - examples/atlas/mathieu/m22.md + - "Mathieu group M23": + - examples/atlas/mathieu/m23/index.md + - "Mathieu group M24": + - examples/atlas/mathieu/m24/index.md + - "Leech lattice groups": + - examples/atlas/leech-lattice/hs.md + - examples/atlas/leech-lattice/j2.md + - "Conway group Co2": + - examples/atlas/leech-lattice/co2/index.md + - "McLaughlin group McL": + - examples/atlas/leech-lattice/mcl/index.md + - "Monster sections": + - "Held group He": + - examples/atlas/monster-sections/he/index.md + - "Fischer group Fi22": + - examples/atlas/monster-sections/fi22/index.md + - "Pariahs": + - examples/atlas/pariahs/j1.md + - examples/atlas/pariahs/j3.md + - "Rudvalis group Ru": + - examples/atlas/pariahs/ru/index.md + - "Janko group J4": + - examples/atlas/pariahs/j4/index.md + - "Miscellaneous": + - examples/atlas/misc/t.md theme: name: material @@ -71,6 +102,10 @@ markdown_extensions: - pymdownx.keys - pymdownx.arithmatex: generic: true + - pymdownx.emoji: + emoji_index: !!python/name:material.extensions.emoji.twemoji + emoji_generator: !!python/name:material.extensions.emoji.to_svg + - pymdownx.tilde copyright: Copyright © 2026 Reinis Cirpons, Joe Edwards and James Mitchell @@ -83,6 +118,9 @@ extra: icon: fontawesome/brands/github link: https://www.github.com/libsemigroups/libsemigroups_pybind11 +extra_css: + - stylesheets/extra.css + extra_javascript: - javascripts/mathjax.js - https://unpkg.com/mathjax@3/es5/tex-mml-chtml.js From 4b2d26e976785c0cbea7754523c4dd2bcad602ef Mon Sep 17 00:00:00 2001 From: Joseph Edwards Date: Tue, 2 Jun 2026 12:38:42 +0100 Subject: [PATCH 4/7] Add TODOs --- docs/examples/atlas/leech-lattice/co2/index.md | 3 +-- docs/examples/atlas/leech-lattice/hs.md | 2 +- docs/examples/atlas/leech-lattice/j2.md | 2 +- docs/examples/atlas/leech-lattice/mcl/index.md | 3 +-- docs/examples/atlas/mathieu/m23/index.md | 3 +-- docs/examples/atlas/mathieu/m24/index.md | 3 +-- docs/examples/atlas/misc/t.md | 3 +-- docs/examples/atlas/monster-sections/fi22/index.md | 3 +-- docs/examples/atlas/monster-sections/he/index.md | 3 +-- docs/examples/atlas/pariahs/j1.md | 2 +- docs/examples/atlas/pariahs/j3.md | 2 +- docs/examples/atlas/pariahs/j4/index.md | 3 +-- docs/examples/atlas/pariahs/ru/index.md | 3 +-- 13 files changed, 13 insertions(+), 22 deletions(-) diff --git a/docs/examples/atlas/leech-lattice/co2/index.md b/docs/examples/atlas/leech-lattice/co2/index.md index e781f66..0c900db 100644 --- a/docs/examples/atlas/leech-lattice/co2/index.md +++ b/docs/examples/atlas/leech-lattice/co2/index.md @@ -2,7 +2,7 @@ > Order: $42,305,421,312,000$ -> Presentation: $\langle{ A \mid R}\rangle$ +> Presentation: TODO On this page, we provide links to verifications that the maximal subgroups of the Conway group Co~2~ define groups of the correct order. @@ -10,4 +10,3 @@ the Conway group Co~2~ define groups of the correct order. ## Maximal subgroups The following are maximal subgroups that have been verified: - diff --git a/docs/examples/atlas/leech-lattice/hs.md b/docs/examples/atlas/leech-lattice/hs.md index 78b5fbf..0f288c3 100644 --- a/docs/examples/atlas/leech-lattice/hs.md +++ b/docs/examples/atlas/leech-lattice/hs.md @@ -2,7 +2,7 @@ > Order: $44,352,000$ -> Presentation: $\langle{ A \mid R}\rangle$ +> Presentation: TODO On this page, we verify that the above claimed presentation of the Higman-Sims group HS defines a group of order $44,352,000$. diff --git a/docs/examples/atlas/leech-lattice/j2.md b/docs/examples/atlas/leech-lattice/j2.md index 691fbd6..4bf4d81 100644 --- a/docs/examples/atlas/leech-lattice/j2.md +++ b/docs/examples/atlas/leech-lattice/j2.md @@ -2,7 +2,7 @@ > Order: $604,800$ -> Presentation: $\langle{ A \mid R}\rangle$ +> Presentation: TODO On this page, we verify that the above claimed presentation of the Janko group J~2~ defines a group of order $604,800$. diff --git a/docs/examples/atlas/leech-lattice/mcl/index.md b/docs/examples/atlas/leech-lattice/mcl/index.md index 4abe0a4..5db3fb3 100644 --- a/docs/examples/atlas/leech-lattice/mcl/index.md +++ b/docs/examples/atlas/leech-lattice/mcl/index.md @@ -2,7 +2,7 @@ > Order: $898,128,000$ -> Presentation: $\langle{ A \mid R}\rangle$ +> Presentation: TODO On this page, we provide links to verifications that the maximal subgroups of the McLaughlin group McL define groups of the correct order. @@ -10,4 +10,3 @@ the McLaughlin group McL define groups of the correct order. ## Maximal subgroups The following are maximal subgroups that have been verified: - diff --git a/docs/examples/atlas/mathieu/m23/index.md b/docs/examples/atlas/mathieu/m23/index.md index c732425..6d877fa 100644 --- a/docs/examples/atlas/mathieu/m23/index.md +++ b/docs/examples/atlas/mathieu/m23/index.md @@ -2,7 +2,7 @@ > Order: $10,200,960$ -> Presentation: $\langle{ A \mid R}\rangle$ +> Presentation: TODO On this page, we provide links to verifications that the maximal subgroups of the Mathieu group M~23~ define groups of the correct order. @@ -10,4 +10,3 @@ the Mathieu group M~23~ define groups of the correct order. ## Maximal subgroups The following are maximal subgroups that have been verified: - diff --git a/docs/examples/atlas/mathieu/m24/index.md b/docs/examples/atlas/mathieu/m24/index.md index 0eb51fb..99166da 100644 --- a/docs/examples/atlas/mathieu/m24/index.md +++ b/docs/examples/atlas/mathieu/m24/index.md @@ -2,7 +2,7 @@ > Order: $244,823,040$ -> Presentation: $\langle{ A \mid R}\rangle$ +> Presentation: TODO On this page, we provide links to verifications that the maximal subgroups of the Mathieu group M~24~ define groups of the correct order. @@ -10,4 +10,3 @@ the Mathieu group M~24~ define groups of the correct order. ## Maximal subgroups The following are maximal subgroups that have been verified: - diff --git a/docs/examples/atlas/misc/t.md b/docs/examples/atlas/misc/t.md index bf48d5b..92815d9 100644 --- a/docs/examples/atlas/misc/t.md +++ b/docs/examples/atlas/misc/t.md @@ -2,7 +2,7 @@ > Order: $17,971,200$ -> Presentation: $\langle{ A \mid R}\rangle$ +> Presentation: TODO On this page, we verify that the above claimed presentation of the Tits group T defines a group of order $17,971,200$. @@ -14,4 +14,3 @@ Coming soon! ## The output Coming soon! - diff --git a/docs/examples/atlas/monster-sections/fi22/index.md b/docs/examples/atlas/monster-sections/fi22/index.md index 4b5681d..042bca6 100644 --- a/docs/examples/atlas/monster-sections/fi22/index.md +++ b/docs/examples/atlas/monster-sections/fi22/index.md @@ -2,7 +2,7 @@ > Order: $64,561,751,654,400$ -> Presentation: $\langle{ A \mid R}\rangle$ +> Presentation: TODO On this page, we provide links to verifications that the maximal subgroups of the Fischer group Fi~22~ define groups of the correct order. @@ -10,4 +10,3 @@ the Fischer group Fi~22~ define groups of the correct order. ## Maximal subgroups The following are maximal subgroups that have been verified: - diff --git a/docs/examples/atlas/monster-sections/he/index.md b/docs/examples/atlas/monster-sections/he/index.md index 357db23..c2f88a7 100644 --- a/docs/examples/atlas/monster-sections/he/index.md +++ b/docs/examples/atlas/monster-sections/he/index.md @@ -2,7 +2,7 @@ > Order: $4,030,387,200$ -> Presentation: $\langle{ A \mid R}\rangle$ +> Presentation: TODO On this page, we provide links to verifications that the maximal subgroups of the Held group He define groups of the correct order. @@ -10,4 +10,3 @@ the Held group He define groups of the correct order. ## Maximal subgroups The following are maximal subgroups that have been verified: - diff --git a/docs/examples/atlas/pariahs/j1.md b/docs/examples/atlas/pariahs/j1.md index d13a34d..5f866fd 100644 --- a/docs/examples/atlas/pariahs/j1.md +++ b/docs/examples/atlas/pariahs/j1.md @@ -2,7 +2,7 @@ > Order: $175,560$ -> Presentation: $\langle{ A \mid R}\rangle$ +> Presentation: TODO On this page, we verify that the above claimed presentation of the Janko group J~1~ defines a group of order $175,560$. diff --git a/docs/examples/atlas/pariahs/j3.md b/docs/examples/atlas/pariahs/j3.md index 0dcdca1..11a96a0 100644 --- a/docs/examples/atlas/pariahs/j3.md +++ b/docs/examples/atlas/pariahs/j3.md @@ -2,7 +2,7 @@ > Order: $50,232,960$ -> Presentation: $\langle{ A \mid R}\rangle$ +> Presentation: TODO On this page, we verify that the above claimed presentation of the Janko group J~3~ defines a group of order $50,232,960$. diff --git a/docs/examples/atlas/pariahs/j4/index.md b/docs/examples/atlas/pariahs/j4/index.md index a80fc7f..5907a8d 100644 --- a/docs/examples/atlas/pariahs/j4/index.md +++ b/docs/examples/atlas/pariahs/j4/index.md @@ -2,7 +2,7 @@ > Order: $86,775,571,046,077,562,880$ -> Presentation: $\langle{ A \mid R}\rangle$ +> Presentation: TODO On this page, we provide links to verifications that the maximal subgroups of the Janko group J~4~ define groups of the correct order. @@ -10,4 +10,3 @@ the Janko group J~4~ define groups of the correct order. ## Maximal subgroups The following are maximal subgroups that have been verified: - diff --git a/docs/examples/atlas/pariahs/ru/index.md b/docs/examples/atlas/pariahs/ru/index.md index b47a2b7..8bc0864 100644 --- a/docs/examples/atlas/pariahs/ru/index.md +++ b/docs/examples/atlas/pariahs/ru/index.md @@ -2,7 +2,7 @@ > Order: $145,926,144,000$ -> Presentation: $\langle{ A \mid R}\rangle$ +> Presentation: TODO On this page, we provide links to verifications that the maximal subgroups of the Rudvalis group Ru define groups of the correct order. @@ -10,4 +10,3 @@ the Rudvalis group Ru define groups of the correct order. ## Maximal subgroups The following are maximal subgroups that have been verified: - From 30e15416e05dab6f44435e293230722afdbf87a9 Mon Sep 17 00:00:00 2001 From: Joseph Edwards Date: Tue, 2 Jun 2026 12:48:14 +0100 Subject: [PATCH 5/7] Rerun scripts --- docs/examples/atlas/mathieu/m11.md | 21 +- docs/examples/atlas/mathieu/m12.md | 93 +++---- docs/examples/atlas/mathieu/m22.md | 423 +++++++++++++---------------- 3 files changed, 239 insertions(+), 298 deletions(-) diff --git a/docs/examples/atlas/mathieu/m11.md b/docs/examples/atlas/mathieu/m11.md index ff62be0..b7a7eeb 100644 --- a/docs/examples/atlas/mathieu/m11.md +++ b/docs/examples/atlas/mathieu/m11.md @@ -33,7 +33,6 @@ tc = ToddCoxeter(congruence_kind.twosided, p) tc.run() assert tc.number_of_classes() == 7920 - ``` ## The output @@ -42,17 +41,15 @@ Running the above script produces the following output: ``` ++++++++++++++++++++++++++++++++ -#0: ToddCoxeter: running for approx. 10.000s -++++++++++++++++++++++++++++++++ #0: ToddCoxeter: RUN 0 START (strategy() = hlt) #0: ToddCoxeter: |A| = 4, |R| = 9, |u| + |v| ∈ [2, 22], ∑(|u| + |v|) = 73 ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.0 START -#0: ToddCoxeter: HLT 0.0.0 | active | killed | defined -#0: ToddCoxeter: nodes | 1 | 0 | 1 -#0: ToddCoxeter: | active | missing | % complete -#0: ToddCoxeter: edges | 0 | 4 | 0.0% -#0: ToddCoxeter: time | run 0 = 19µs | all runs = 19µs | elapsed = 641µs +#0: ToddCoxeter: HLT 0.0.0 | active | killed | defined +#0: ToddCoxeter: nodes | 1 | 0 | 1 +#0: ToddCoxeter: | active | missing | % complete +#0: ToddCoxeter: edges | 0 | 4 | 0.0% +#0: ToddCoxeter: time | run 0 = 28µs | all runs = 28µs | elapsed = 92µs ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.0 STOP #0: ToddCoxeter: HLT 0.0.1 | active | killed | defined @@ -61,7 +58,7 @@ Running the above script produces the following output: #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 31,680 | 0 | 100.0% #0: ToddCoxeter: diff 0.0.0 | +31,680 | -4 | +100.0% -#0: ToddCoxeter: phase 0.0 = 209ms | run 0 = 209ms | all runs = 209ms | elapsed = 210ms +#0: ToddCoxeter: phase 0.0 = 176ms | run 0 = 176ms | all runs = 176ms | elapsed = 176ms ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.1.2 | active | killed | defined #0: ToddCoxeter: nodes | 7,920 | 1,992,427 | 2,000,347 @@ -71,13 +68,13 @@ Running the above script produces the following output: #0: ToddCoxeter: edges | 31,680 | 0 | 100.0% #0: ToddCoxeter: diff 0.1.1 | +0 | +0 | +0.0% #0: ToddCoxeter: diff 0.1.0 | +31,680 | -4 | +100.0% -#0: ToddCoxeter: phase 0.1 = 209ms | run 0 = 209ms | all runs = 209ms | elapsed = 210ms +#0: ToddCoxeter: phase 0.1 = 176ms | run 0 = 176ms | all runs = 176ms | elapsed = 176ms ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: RUN 0 STOP (finished) #0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch #0: ToddCoxeter: num. phases | 0 | 0 | 1 | 0 -#0: ToddCoxeter: time spent in phases | - (0%) | - (0%) | 209ms (100%) | - (0%) -#0: ToddCoxeter: phase 0.1 = 209ms | run 0 = 209ms | all runs = 209ms | elapsed = 210ms +#0: ToddCoxeter: time spent in phases | - (0%) | - (0%) | 176ms (100%) | - (0%) +#0: ToddCoxeter: phase 0.1 = 176ms | run 0 = 176ms | all runs = 176ms | elapsed = 176ms ``` :simple-ticktick: The computed size of the group matches the size of the group diff --git a/docs/examples/atlas/mathieu/m12.md b/docs/examples/atlas/mathieu/m12.md index 9868ad0..9235cb5 100644 --- a/docs/examples/atlas/mathieu/m12.md +++ b/docs/examples/atlas/mathieu/m12.md @@ -31,7 +31,7 @@ presentation.add_rule(p, parse_relations("(ababaB)^6"), "") # Run the Todd-Coxeter algorithm tc = ToddCoxeter(congruence_kind.twosided, p) -tc.run_for() +tc.run() assert tc.number_of_classes() == 95040 ``` @@ -44,17 +44,15 @@ Running the above script produces the following output: ``` ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: running for approx. 10.000s - ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: RUN 0 START (strategy() = hlt) #0: ToddCoxeter: |A| = 4, |R| = 9, |u| + |v| ∈ [2, 36], ∑(|u| + |v|) = 95 ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.0 START - #0: ToddCoxeter: HLT 0.0.0 | active | killed | defined - #0: ToddCoxeter: nodes | 1 | 0 | 1 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 0 | 4 | 0.0% - #0: ToddCoxeter: time | run 0 = 21µs | all runs = 21µs | elapsed = 103µs + #0: ToddCoxeter: HLT 0.0.0 | active | killed | defined + #0: ToddCoxeter: nodes | 1 | 0 | 1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 0 | 4 | 0.0% + #0: ToddCoxeter: time | run 0 = 24µs | all runs = 24µs | elapsed = 84µs ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.0 STOP #0: ToddCoxeter: HLT 0.0.1 | active | killed | defined @@ -63,38 +61,27 @@ Running the above script produces the following output: #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 5,782,533 | 14,217,483 | 28.9% #0: ToddCoxeter: diff 0.0.0 | +5,782,533 | +14,217,479 | +28.9% - #0: ToddCoxeter: phase 0.0 = 624ms | run 0 = 624ms | all runs = 624ms | elapsed = 624ms + #0: ToddCoxeter: phase 0.0 = 489ms | run 0 = 489ms | all runs = 489ms | elapsed = 489ms ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.1 START (lookahead_extent() = partial, lookahead_style() = hlt) #0: ToddCoxeter: LOOKAHEAD 0.1.0 | active | killed | defined #0: ToddCoxeter: nodes | 5,000,004 | 2,964,327 | 7,964,331 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 5,782,533 | 14,217,483 | 28.9% - #0: ToddCoxeter: time | run 0 = 624ms | all runs = 624ms | elapsed = 624ms + #0: ToddCoxeter: time | run 0 = 489ms | all runs = 489ms | elapsed = 489ms #0: ToddCoxeter: because a >= n #0: ToddCoxeter: where: a = number_of_nodes_active() = 5,000,004 #0: ToddCoxeter: n = lookahead_next() = 5,000,000 #0: ToddCoxeter: large collapse, number of coincidences 100,002 >= 100,000 = large_collapse()! ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.1.1 | active | killed | defined - #1: ToddCoxeter: nodes | 1,909,907 | 6,057,700 | 7,964,331 - #1: ToddCoxeter: diff 0.1.0 | -3,090,097 | +3,093,373 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 0 | 7,639,628 | 0.0% - #1: ToddCoxeter: diff 0.1.0 | -5,782,533 | -6,577,855 | -28.9% - #1: ToddCoxeter: phase 0.1 = 375ms | run 0 = 1.001s | all runs = 1.001s | elapsed = 1.001s - #1: ToddCoxeter: lookahead progress | ~32.6% - ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.1 STOP - #0: ToddCoxeter: LOOKAHEAD 0.1.2 | active | killed | defined - #0: ToddCoxeter: nodes | 95,046 | 7,869,285 | 7,964,331 - #0: ToddCoxeter: diff 0.1.1 | -1,814,861 | +1,811,585 | +0 - #0: ToddCoxeter: diff 0.1.0 | -4,904,958 | +4,904,958 | +0 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 380,177 | 7 | 100.0% - #0: ToddCoxeter: diff 0.1.1 | +380,177 | -7,639,621 | +100.0% - #0: ToddCoxeter: diff 0.1.0 | -5,402,356 | -14,217,476 | +71.1% - #0: ToddCoxeter: phase 0.1 = 491ms | run 0 = 1.116s | all runs = 1.116s | elapsed = 1.116s + #0: ToddCoxeter: LOOKAHEAD 0.1.1 | active | killed | defined + #0: ToddCoxeter: nodes | 95,046 | 7,869,285 | 7,964,331 + #0: ToddCoxeter: diff 0.1.0 | -4,904,958 | +4,904,958 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,177 | 7 | 100.0% + #0: ToddCoxeter: diff 0.1.0 | -5,402,356 | -14,217,476 | +71.1% + #0: ToddCoxeter: phase 0.1 = 449ms | run 0 = 939ms | all runs = 939ms | elapsed = 939ms #0: ToddCoxeter: lookahead_next() is now max(f x a = 190,092, m = 10,000) (-4,809,908) #0: ToddCoxeter: because f x a < n #0: ToddCoxeter: where: a = number_of_nodes_active() = 95,046 @@ -103,36 +90,36 @@ Running the above script produces the following output: #0: ToddCoxeter: n = lookahead_next() = 5,000,000 ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.2 START - #0: ToddCoxeter: HLT 0.2.0 | active | killed | defined - #0: ToddCoxeter: nodes | 95,046 | 7,869,285 | 7,964,331 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 380,177 | 7 | 100.0% - #0: ToddCoxeter: time | run 0 = 1.116s | all runs = 1.116s | elapsed = 1.116s + #0: ToddCoxeter: HLT 0.2.0 | active | killed | defined + #0: ToddCoxeter: nodes | 95,046 | 7,869,285 | 7,964,331 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,177 | 7 | 100.0% + #0: ToddCoxeter: time | run 0 = 939ms | all runs = 939ms | elapsed = 939ms ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.2 STOP - #0: ToddCoxeter: HLT 0.2.1 | active | killed | defined - #0: ToddCoxeter: nodes | 95,040 | 7,869,292 | 7,964,332 - #0: ToddCoxeter: diff 0.2.0 | -6 | +7 | +1 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 380,160 | 0 | 100.0% - #0: ToddCoxeter: diff 0.2.0 | -17 | -7 | +0.0% - #0: ToddCoxeter: phase 0.2 = 19ms | run 0 = 1.136s | all runs = 1.136s | elapsed = 1.136s + #0: ToddCoxeter: HLT 0.2.1 | active | killed | defined + #0: ToddCoxeter: nodes | 95,040 | 7,869,292 | 7,964,332 + #0: ToddCoxeter: diff 0.2.0 | -6 | +7 | +1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,160 | 0 | 100.0% + #0: ToddCoxeter: diff 0.2.0 | -17 | -7 | +0.0% + #0: ToddCoxeter: phase 0.2 = 13ms | run 0 = 952ms | all runs = 952ms | elapsed = 952ms ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.3.2 | active | killed | defined - #0: ToddCoxeter: nodes | 95,040 | 7,869,292 | 7,964,332 - #0: ToddCoxeter: diff 0.3.1 | +0 | +0 | +0 - #0: ToddCoxeter: diff 0.3.0 | -6 | +7 | +1 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 380,160 | 0 | 100.0% - #0: ToddCoxeter: diff 0.3.1 | +0 | +0 | +0.0% - #0: ToddCoxeter: diff 0.3.0 | -17 | -7 | +0.0% - #0: ToddCoxeter: phase 0.3 = 19ms | run 0 = 1.136s | all runs = 1.136s | elapsed = 1.136s + #0: ToddCoxeter: HLT 0.3.2 | active | killed | defined + #0: ToddCoxeter: nodes | 95,040 | 7,869,292 | 7,964,332 + #0: ToddCoxeter: diff 0.3.1 | +0 | +0 | +0 + #0: ToddCoxeter: diff 0.3.0 | -6 | +7 | +1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,160 | 0 | 100.0% + #0: ToddCoxeter: diff 0.3.1 | +0 | +0 | +0.0% + #0: ToddCoxeter: diff 0.3.0 | -17 | -7 | +0.0% + #0: ToddCoxeter: phase 0.3 = 13ms | run 0 = 952ms | all runs = 952ms | elapsed = 952ms ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: RUN 0 STOP (finished) - #0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch - #0: ToddCoxeter: num. phases | 1 | 0 | 2 | 0 - #0: ToddCoxeter: time spent in phases | 491ms (43%) | - (0%) | 644ms (57%) | - (0%) - #0: ToddCoxeter: phase 0.3 = 20ms | run 0 = 1.137s | all runs = 1.137s | elapsed = 1.137s + #0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch + #0: ToddCoxeter: num. phases | 1 | 0 | 2 | 0 + #0: ToddCoxeter: time spent in phases | 449ms (47%) | - (0%) | 502ms (53%) | - (0%) + #0: ToddCoxeter: phase 0.3 = 14ms | run 0 = 953ms | all runs = 953ms | elapsed = 953ms ``` :simple-ticktick: The computed size of the group matches the size of the group diff --git a/docs/examples/atlas/mathieu/m22.md b/docs/examples/atlas/mathieu/m22.md index f32d718..6d9422a 100644 --- a/docs/examples/atlas/mathieu/m22.md +++ b/docs/examples/atlas/mathieu/m22.md @@ -45,8 +45,6 @@ Running the above script produces the following output: ``` ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: running for approx. 30.000s - ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: RUN 0 START (strategy() = hlt) #0: ToddCoxeter: |A| = 4, |R| = 10, |u| + |v| ∈ [2, 30], ∑(|u| + |v|) = 105 ++++++++++++++++++++++++++++++++ @@ -55,7 +53,7 @@ Running the above script produces the following output: #0: ToddCoxeter: nodes | 1 | 0 | 1 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 0 | 4 | 0.0% - #0: ToddCoxeter: time | run 0 = 19µs | all runs = 19µs | elapsed = 89µs + #0: ToddCoxeter: time | run 0 = 23µs | all runs = 23µs | elapsed = 78µs ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.0 STOP #0: ToddCoxeter: HLT 0.0.1 | active | killed | defined @@ -64,37 +62,26 @@ Running the above script produces the following output: #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 5,679,076 | 14,320,996 | 28.4% #0: ToddCoxeter: diff 0.0.0 | +5,679,076 | +14,320,992 | +28.4% - #0: ToddCoxeter: phase 0.0 = 547ms | run 0 = 547ms | all runs = 547ms | elapsed = 547ms + #0: ToddCoxeter: phase 0.0 = 418ms | run 0 = 418ms | all runs = 418ms | elapsed = 418ms ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.1 START (lookahead_extent() = partial, lookahead_style() = hlt) #0: ToddCoxeter: LOOKAHEAD 0.1.0 | active | killed | defined #0: ToddCoxeter: nodes | 5,000,018 | 1,632,158 | 6,632,176 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 5,679,076 | 14,320,996 | 28.4% - #0: ToddCoxeter: time | run 0 = 547ms | all runs = 547ms | elapsed = 547ms + #0: ToddCoxeter: time | run 0 = 418ms | all runs = 418ms | elapsed = 418ms #0: ToddCoxeter: because a >= n #0: ToddCoxeter: where: a = number_of_nodes_active() = 5,000,018 #0: ToddCoxeter: n = lookahead_next() = 5,000,000 ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.1.1 | active | killed | defined - #1: ToddCoxeter: nodes | 2,644,921 | 3,987,547 | 6,632,176 - #1: ToddCoxeter: diff 0.1.0 | -2,355,097 | +2,355,389 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 7,553,691 | 3,025,993 | 71.4% - #1: ToddCoxeter: diff 0.1.0 | +1,874,615 | -11,295,003 | +43.0% - #1: ToddCoxeter: phase 0.1 = 452ms | run 0 = 1.000s | all runs = 1.000s | elapsed = 1.001s - #1: ToddCoxeter: lookahead progress | ~60.5% - ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.1 STOP - #0: ToddCoxeter: LOOKAHEAD 0.1.2 | active | killed | defined - #0: ToddCoxeter: nodes | 2,423,713 | 4,208,463 | 6,632,176 - #0: ToddCoxeter: diff 0.1.1 | -221,208 | +220,916 | +0 - #0: ToddCoxeter: diff 0.1.0 | -2,576,305 | +2,576,305 | +0 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 7,815,443 | 1,879,409 | 80.6% - #0: ToddCoxeter: diff 0.1.1 | +261,752 | -1,146,584 | +9.2% - #0: ToddCoxeter: diff 0.1.0 | +2,136,367 | -12,441,587 | +52.2% - #0: ToddCoxeter: phase 0.1 = 500ms | run 0 = 1.049s | all runs = 1.049s | elapsed = 1.049s + #0: ToddCoxeter: LOOKAHEAD 0.1.1 | active | killed | defined + #0: ToddCoxeter: nodes | 2,423,713 | 4,208,463 | 6,632,176 + #0: ToddCoxeter: diff 0.1.0 | -2,576,305 | +2,576,305 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 7,815,443 | 1,879,409 | 80.6% + #0: ToddCoxeter: diff 0.1.0 | +2,136,367 | -12,441,587 | +52.2% + #0: ToddCoxeter: phase 0.1 = 398ms | run 0 = 816ms | all runs = 816ms | elapsed = 816ms #0: ToddCoxeter: lookahead_next() is now max(f x a = 4,847,426, m = 10,000) (-152,574) #0: ToddCoxeter: because f x a < n #0: ToddCoxeter: where: a = number_of_nodes_active() = 2,423,713 @@ -103,39 +90,50 @@ Running the above script produces the following output: #0: ToddCoxeter: n = lookahead_next() = 5,000,000 ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.2 START - #0: ToddCoxeter: HLT 0.2.0 | active | killed | defined - #0: ToddCoxeter: nodes | 2,423,713 | 4,208,463 | 6,632,176 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 7,815,443 | 1,879,409 | 80.6% - #0: ToddCoxeter: time | run 0 = 1.049s | all runs = 1.049s | elapsed = 1.049s + #0: ToddCoxeter: HLT 0.2.0 | active | killed | defined + #0: ToddCoxeter: nodes | 2,423,713 | 4,208,463 | 6,632,176 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 7,815,443 | 1,879,409 | 80.6% + #0: ToddCoxeter: time | run 0 = 816ms | all runs = 816ms | elapsed = 816ms ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.2 STOP - #0: ToddCoxeter: HLT 0.2.1 | active | killed | defined - #0: ToddCoxeter: nodes | 4,847,474 | 4,320,458 | 9,167,932 - #0: ToddCoxeter: diff 0.2.0 | +2,423,761 | +111,995 | +2,535,756 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 10,422,837 | 8,967,059 | 53.8% - #0: ToddCoxeter: diff 0.2.0 | +2,607,394 | +7,087,650 | -26.9% - #0: ToddCoxeter: phase 0.2 = 89ms | run 0 = 1.138s | all runs = 1.138s | elapsed = 1.138s + #0: ToddCoxeter: HLT 0.2.1 | active | killed | defined + #0: ToddCoxeter: nodes | 4,847,474 | 4,320,458 | 9,167,932 + #0: ToddCoxeter: diff 0.2.0 | +2,423,761 | +111,995 | +2,535,756 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 10,422,837 | 8,967,059 | 53.8% + #0: ToddCoxeter: diff 0.2.0 | +2,607,394 | +7,087,650 | -26.9% + #0: ToddCoxeter: phase 0.2 = 78ms | run 0 = 894ms | all runs = 894ms | elapsed = 894ms ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.3 START (lookahead_extent() = partial, lookahead_style() = hlt) - #0: ToddCoxeter: LOOKAHEAD 0.3.0 | active | killed | defined - #0: ToddCoxeter: nodes | 4,847,474 | 4,320,458 | 9,167,932 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 10,422,837 | 8,967,059 | 53.8% - #0: ToddCoxeter: time | run 0 = 1.138s | all runs = 1.138s | elapsed = 1.138s + #0: ToddCoxeter: LOOKAHEAD 0.3.0 | active | killed | defined + #0: ToddCoxeter: nodes | 4,847,474 | 4,320,458 | 9,167,932 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 10,422,837 | 8,967,059 | 53.8% + #0: ToddCoxeter: time | run 0 = 894ms | all runs = 894ms | elapsed = 894ms #0: ToddCoxeter: because a >= n #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,847,474 #0: ToddCoxeter: n = lookahead_next() = 4,847,426 ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.3.1 | active | killed | defined + #1: ToddCoxeter: nodes | 4,720,512 | 4,447,422 | 9,167,932 + #1: ToddCoxeter: diff 0.3.0 | -126,962 | +126,964 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 10,288,113 | 8,593,935 | 54.5% + #1: ToddCoxeter: diff 0.3.0 | -134,724 | -373,124 | +0.7% + #1: ToddCoxeter: phase 0.3 = 105ms | run 0 = 1.000s | all runs = 1.000s | elapsed = 1.000s + #1: ToddCoxeter: lookahead progress | ~17.5% + ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.3 STOP - #0: ToddCoxeter: LOOKAHEAD 0.3.1 | active | killed | defined + #0: ToddCoxeter: LOOKAHEAD 0.3.2 | active | killed | defined #0: ToddCoxeter: nodes | 3,512,400 | 5,655,532 | 9,167,932 + #0: ToddCoxeter: diff 0.3.1 | -1,208,112 | +1,208,110 | +0 #0: ToddCoxeter: diff 0.3.0 | -1,335,074 | +1,335,074 | +0 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 11,491,787 | 2,557,813 | 81.8% + #0: ToddCoxeter: diff 0.3.1 | +1,203,674 | -6,036,122 | +27.3% #0: ToddCoxeter: diff 0.3.0 | +1,068,950 | -6,409,246 | +28.0% - #0: ToddCoxeter: phase 0.3 = 718ms | run 0 = 1.856s | all runs = 1.856s | elapsed = 1.857s + #0: ToddCoxeter: phase 0.3 = 556ms | run 0 = 1.451s | all runs = 1.451s | elapsed = 1.451s #0: ToddCoxeter: lookahead_next() is now 4,847,426 (+0) #0: ToddCoxeter: because: #0: ToddCoxeter: 1. n <= f x a = 7,024,800 @@ -152,7 +150,7 @@ Running the above script produces the following output: #0: ToddCoxeter: nodes | 3,512,400 | 5,655,532 | 9,167,932 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 11,491,787 | 2,557,813 | 81.8% - #0: ToddCoxeter: time | run 0 = 1.857s | all runs = 1.857s | elapsed = 1.857s + #0: ToddCoxeter: time | run 0 = 1.451s | all runs = 1.451s | elapsed = 1.451s ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.4 STOP #0: ToddCoxeter: HLT 0.4.1 | active | killed | defined @@ -161,37 +159,37 @@ Running the above script produces the following output: #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 12,934,269 | 6,455,527 | 66.7% #0: ToddCoxeter: diff 0.4.0 | +1,442,482 | +3,897,714 | -15.1% - #0: ToddCoxeter: phase 0.4 = 67ms | run 0 = 1.924s | all runs = 1.924s | elapsed = 1.924s + #0: ToddCoxeter: phase 0.4 = 62ms | run 0 = 1.513s | all runs = 1.513s | elapsed = 1.514s ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.5 START (lookahead_extent() = partial, lookahead_style() = hlt) #0: ToddCoxeter: LOOKAHEAD 0.5.0 | active | killed | defined #0: ToddCoxeter: nodes | 4,847,449 | 5,703,629 | 10,551,078 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 12,934,269 | 6,455,527 | 66.7% - #0: ToddCoxeter: time | run 0 = 1.924s | all runs = 1.924s | elapsed = 1.924s + #0: ToddCoxeter: time | run 0 = 1.513s | all runs = 1.513s | elapsed = 1.514s #0: ToddCoxeter: because a >= n #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,847,449 #0: ToddCoxeter: n = lookahead_next() = 4,847,426 ++++++++++++++++++++++++++++++++ #1: ToddCoxeter: LOOKAHEAD 0.5.1 | active | killed | defined - #1: ToddCoxeter: nodes | 4,820,487 | 5,730,591 | 10,551,078 - #1: ToddCoxeter: diff 0.5.0 | -26,962 | +26,962 | +0 + #1: ToddCoxeter: nodes | 4,565,240 | 5,985,863 | 10,551,078 + #1: ToddCoxeter: diff 0.5.0 | -282,209 | +282,234 | +0 #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 12,908,450 | 6,373,498 | 66.9% - #1: ToddCoxeter: diff 0.5.0 | -25,819 | -82,029 | +0.2% - #1: ToddCoxeter: phase 0.5 = 77ms | run 0 = 2.001s | all runs = 2.001s | elapsed = 2.001s - #1: ToddCoxeter: lookahead progress | ~11.0% + #1: ToddCoxeter: edges | 13,023,236 | 5,237,724 | 71.3% + #1: ToddCoxeter: diff 0.5.0 | +88,967 | -1,217,803 | +4.6% + #1: ToddCoxeter: phase 0.5 = 487ms | run 0 = 2.001s | all runs = 2.001s | elapsed = 2.001s + #1: ToddCoxeter: lookahead progress | ~77.2% ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.5 STOP #0: ToddCoxeter: LOOKAHEAD 0.5.2 | active | killed | defined #0: ToddCoxeter: nodes | 4,134,106 | 6,416,972 | 10,551,078 - #0: ToddCoxeter: diff 0.5.1 | -686,381 | +686,381 | +0 + #0: ToddCoxeter: diff 0.5.1 | -431,134 | +431,109 | +0 #0: ToddCoxeter: diff 0.5.0 | -713,343 | +713,343 | +0 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 13,557,552 | 2,978,872 | 82.0% - #0: ToddCoxeter: diff 0.5.1 | +649,102 | -3,394,626 | +15.0% + #0: ToddCoxeter: diff 0.5.1 | +534,316 | -2,258,852 | +10.7% #0: ToddCoxeter: diff 0.5.0 | +623,283 | -3,476,655 | +15.3% - #0: ToddCoxeter: phase 0.5 = 856ms | run 0 = 2.780s | all runs = 2.780s | elapsed = 2.780s + #0: ToddCoxeter: phase 0.5 = 642ms | run 0 = 2.156s | all runs = 2.156s | elapsed = 2.156s #0: ToddCoxeter: lookahead_next() is now n x f = 9,694,852 (+4,847,426) #0: ToddCoxeter: because: l < (l + a) / t = 1,211,862 #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,134,106 @@ -205,56 +203,46 @@ Running the above script produces the following output: #0: ToddCoxeter: nodes | 4,134,106 | 6,416,972 | 10,551,078 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 13,557,552 | 2,978,872 | 82.0% - #0: ToddCoxeter: time | run 0 = 2.780s | all runs = 2.780s | elapsed = 2.780s - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: HLT 0.6.1 | active | killed | defined - #1: ToddCoxeter: nodes | 8,388,608 | 6,594,998 | 14,983,606 - #1: ToddCoxeter: diff 0.6.0 | +4,254,502 | +178,026 | +4,432,528 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 18,160,579 | 15,393,853 | 54.1% - #1: ToddCoxeter: diff 0.6.0 | +4,603,027 | +12,414,981 | -27.9% - #1: ToddCoxeter: phase 0.6 = 221ms | run 0 = 3.001s | all runs = 3.001s | elapsed = 3.001s + #0: ToddCoxeter: time | run 0 = 2.156s | all runs = 2.156s | elapsed = 2.156s ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.6 STOP - #0: ToddCoxeter: HLT 0.6.2 | active | killed | defined + #0: ToddCoxeter: HLT 0.6.1 | active | killed | defined #0: ToddCoxeter: nodes | 9,694,873 | 6,657,105 | 16,351,978 - #0: ToddCoxeter: diff 0.6.1 | +1,306,265 | +62,107 | +1,368,372 #0: ToddCoxeter: diff 0.6.0 | +5,560,767 | +240,133 | +5,800,900 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 19,575,370 | 19,204,122 | 50.5% - #0: ToddCoxeter: diff 0.6.1 | +1,414,791 | +3,810,269 | -3.6% #0: ToddCoxeter: diff 0.6.0 | +6,017,818 | +16,225,250 | -31.5% - #0: ToddCoxeter: phase 0.6 = 520ms | run 0 = 3.301s | all runs = 3.301s | elapsed = 3.301s + #0: ToddCoxeter: phase 0.6 = 425ms | run 0 = 2.582s | all runs = 2.582s | elapsed = 2.582s ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.7 START (lookahead_extent() = partial, lookahead_style() = hlt) #0: ToddCoxeter: LOOKAHEAD 0.7.0 | active | killed | defined #0: ToddCoxeter: nodes | 9,694,873 | 6,657,105 | 16,351,978 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 19,575,370 | 19,204,122 | 50.5% - #0: ToddCoxeter: time | run 0 = 3.301s | all runs = 3.301s | elapsed = 3.301s + #0: ToddCoxeter: time | run 0 = 2.582s | all runs = 2.582s | elapsed = 2.582s #0: ToddCoxeter: because a >= n #0: ToddCoxeter: where: a = number_of_nodes_active() = 9,694,873 #0: ToddCoxeter: n = lookahead_next() = 9,694,852 ++++++++++++++++++++++++++++++++ #1: ToddCoxeter: LOOKAHEAD 0.7.1 | active | killed | defined - #1: ToddCoxeter: nodes | 9,431,978 | 6,920,002 | 16,351,978 - #1: ToddCoxeter: diff 0.7.0 | -262,895 | +262,897 | +0 + #1: ToddCoxeter: nodes | 9,521,847 | 6,830,131 | 16,351,978 + #1: ToddCoxeter: diff 0.7.0 | -173,026 | +173,026 | +0 #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 19,360,399 | 18,367,513 | 51.3% - #1: ToddCoxeter: diff 0.7.0 | -214,971 | -836,609 | +0.8% - #1: ToddCoxeter: phase 0.7 = 700ms | run 0 = 4.001s | all runs = 4.001s | elapsed = 4.001s - #1: ToddCoxeter: lookahead progress | ~41.5% + #1: ToddCoxeter: edges | 19,432,594 | 18,654,794 | 51.0% + #1: ToddCoxeter: diff 0.7.0 | -142,776 | -549,328 | +0.5% + #1: ToddCoxeter: phase 0.7 = 418ms | run 0 = 3.001s | all runs = 3.001s | elapsed = 3.001s + #1: ToddCoxeter: lookahead progress | ~33.5% ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.7 STOP #0: ToddCoxeter: LOOKAHEAD 0.7.2 | active | killed | defined #0: ToddCoxeter: nodes | 6,784,030 | 9,567,948 | 16,351,978 - #0: ToddCoxeter: diff 0.7.1 | -2,647,948 | +2,647,946 | +0 + #0: ToddCoxeter: diff 0.7.1 | -2,737,817 | +2,737,817 | +0 #0: ToddCoxeter: diff 0.7.0 | -2,910,843 | +2,910,843 | +0 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 22,154,799 | 4,981,321 | 81.6% - #0: ToddCoxeter: diff 0.7.1 | +2,794,400 | -13,386,192 | +30.3% + #0: ToddCoxeter: diff 0.7.1 | +2,722,205 | -13,673,473 | +30.6% #0: ToddCoxeter: diff 0.7.0 | +2,579,429 | -14,222,801 | +31.2% - #0: ToddCoxeter: phase 0.7 = 1.445s | run 0 = 4.746s | all runs = 4.746s | elapsed = 4.746s + #0: ToddCoxeter: phase 0.7 = 1.109s | run 0 = 3.691s | all runs = 3.691s | elapsed = 3.691s #0: ToddCoxeter: lookahead_next() is now 9,694,852 (+0) #0: ToddCoxeter: because: #0: ToddCoxeter: 1. n <= f x a = 13,568,060 @@ -271,7 +259,7 @@ Running the above script produces the following output: #0: ToddCoxeter: nodes | 6,784,030 | 9,567,948 | 16,351,978 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 22,154,799 | 4,981,321 | 81.6% - #0: ToddCoxeter: time | run 0 = 4.746s | all runs = 4.746s | elapsed = 4.746s + #0: ToddCoxeter: time | run 0 = 3.691s | all runs = 3.691s | elapsed = 3.691s ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.8 STOP #0: ToddCoxeter: HLT 0.8.1 | active | killed | defined @@ -280,48 +268,48 @@ Running the above script produces the following output: #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 25,297,258 | 13,482,158 | 65.2% #0: ToddCoxeter: diff 0.8.0 | +3,142,459 | +8,500,837 | -16.4% - #0: ToddCoxeter: phase 0.8 = 130ms | run 0 = 4.876s | all runs = 4.876s | elapsed = 4.876s + #0: ToddCoxeter: phase 0.8 = 113ms | run 0 = 3.805s | all runs = 3.805s | elapsed = 3.805s ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.9 START (lookahead_extent() = partial, lookahead_style() = hlt) #0: ToddCoxeter: LOOKAHEAD 0.9.0 | active | killed | defined #0: ToddCoxeter: nodes | 9,694,854 | 9,675,719 | 19,370,573 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 25,297,258 | 13,482,158 | 65.2% - #0: ToddCoxeter: time | run 0 = 4.876s | all runs = 4.876s | elapsed = 4.876s + #0: ToddCoxeter: time | run 0 = 3.805s | all runs = 3.805s | elapsed = 3.805s #0: ToddCoxeter: because a >= n #0: ToddCoxeter: where: a = number_of_nodes_active() = 9,694,854 #0: ToddCoxeter: n = lookahead_next() = 9,694,852 ++++++++++++++++++++++++++++++++ #1: ToddCoxeter: LOOKAHEAD 0.9.1 | active | killed | defined - #1: ToddCoxeter: nodes | 9,648,811 | 9,721,762 | 19,370,573 - #1: ToddCoxeter: diff 0.9.0 | -46,043 | +46,043 | +0 + #1: ToddCoxeter: nodes | 9,601,434 | 9,769,139 | 19,370,573 + #1: ToddCoxeter: diff 0.9.0 | -93,420 | +93,420 | +0 #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 25,256,260 | 13,338,984 | 65.4% - #1: ToddCoxeter: diff 0.9.0 | -40,998 | -143,174 | +0.2% - #1: ToddCoxeter: phase 0.9 = 125ms | run 0 = 5.001s | all runs = 5.001s | elapsed = 5.002s - #1: ToddCoxeter: lookahead progress | ~9.5% + #1: ToddCoxeter: edges | 25,215,676 | 13,190,060 | 65.7% + #1: ToddCoxeter: diff 0.9.0 | -81,582 | -292,098 | +0.4% + #1: ToddCoxeter: phase 0.9 = 196ms | run 0 = 4.001s | all runs = 4.001s | elapsed = 4.001s + #1: ToddCoxeter: lookahead progress | ~16.5% ++++++++++++++++++++++++++++++++ #1: ToddCoxeter: LOOKAHEAD 0.9.2 | active | killed | defined - #1: ToddCoxeter: nodes | 9,403,427 | 9,967,160 | 19,370,573 - #1: ToddCoxeter: diff 0.9.1 | -245,384 | +245,398 | +0 - #1: ToddCoxeter: diff 0.9.0 | -291,427 | +291,441 | +0 + #1: ToddCoxeter: nodes | 8,331,834 | 11,038,768 | 19,370,573 + #1: ToddCoxeter: diff 0.9.1 | -1,269,600 | +1,269,629 | +0 + #1: ToddCoxeter: diff 0.9.0 | -1,363,020 | +1,363,049 | +0 #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 25,010,253 | 12,603,455 | 66.5% - #1: ToddCoxeter: diff 0.9.1 | -246,007 | -735,529 | +1.1% - #1: ToddCoxeter: diff 0.9.0 | -287,005 | -878,703 | +1.3% - #1: ToddCoxeter: phase 0.9 = 1.126s | run 0 = 6.002s | all runs = 6.002s | elapsed = 6.002s - #1: ToddCoxeter: lookahead progress | ~63.4% + #1: ToddCoxeter: edges | 26,231,811 | 7,095,525 | 78.7% + #1: ToddCoxeter: diff 0.9.1 | +1,016,135 | -6,094,535 | +13.1% + #1: ToddCoxeter: diff 0.9.0 | +934,553 | -6,386,633 | +13.5% + #1: ToddCoxeter: phase 0.9 = 1.197s | run 0 = 5.001s | all runs = 5.001s | elapsed = 5.001s + #1: ToddCoxeter: lookahead progress | ~87.1% ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.9 STOP #0: ToddCoxeter: LOOKAHEAD 0.9.3 | active | killed | defined #0: ToddCoxeter: nodes | 8,086,523 | 11,284,050 | 19,370,573 - #0: ToddCoxeter: diff 0.9.2 | -1,316,904 | +1,316,890 | +0 + #0: ToddCoxeter: diff 0.9.2 | -245,311 | +245,282 | +0 #0: ToddCoxeter: diff 0.9.0 | -1,608,331 | +1,608,331 | +0 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 26,555,088 | 5,791,004 | 82.1% - #0: ToddCoxeter: diff 0.9.2 | +1,544,835 | -6,812,451 | +15.6% + #0: ToddCoxeter: diff 0.9.2 | +323,277 | -1,304,521 | +3.4% #0: ToddCoxeter: diff 0.9.0 | +1,257,830 | -7,691,154 | +16.9% - #0: ToddCoxeter: phase 0.9 = 1.690s | run 0 = 6.566s | all runs = 6.566s | elapsed = 6.566s + #0: ToddCoxeter: phase 0.9 = 1.320s | run 0 = 5.125s | all runs = 5.125s | elapsed = 5.125s #0: ToddCoxeter: lookahead_next() is now n x f = 19,389,704 (+9,694,852) #0: ToddCoxeter: because: l < (l + a) / t = 2,423,713 #0: ToddCoxeter: where: a = number_of_nodes_active() = 8,086,523 @@ -335,78 +323,68 @@ Running the above script produces the following output: #0: ToddCoxeter: nodes | 8,086,523 | 11,284,050 | 19,370,573 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 26,555,088 | 5,791,004 | 82.1% - #0: ToddCoxeter: time | run 0 = 6.566s | all runs = 6.566s | elapsed = 6.566s - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: HLT 0.10.1 | active | killed | defined - #1: ToddCoxeter: nodes | 16,777,216 | 11,642,699 | 28,419,915 - #1: ToddCoxeter: diff 0.10.0 | +8,690,693 | +358,649 | +9,049,342 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 35,954,563 | 31,154,301 | 53.6% - #1: ToddCoxeter: diff 0.10.0 | +9,399,475 | +25,363,297 | -28.5% - #1: ToddCoxeter: phase 0.10 = 436ms | run 0 = 7.002s | all runs = 7.002s | elapsed = 7.002s + #0: ToddCoxeter: time | run 0 = 5.125s | all runs = 5.125s | elapsed = 5.125s ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.10 STOP - #0: ToddCoxeter: HLT 0.10.2 | active | killed | defined - #0: ToddCoxeter: nodes | 19,389,750 | 11,773,835 | 31,163,585 - #0: ToddCoxeter: diff 0.10.1 | +2,612,534 | +131,136 | +2,743,670 - #0: ToddCoxeter: diff 0.10.0 | +11,303,227 | +489,785 | +11,793,012 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 38,786,740 | 38,772,260 | 50.0% - #0: ToddCoxeter: diff 0.10.1 | +2,832,177 | +7,617,959 | -3.6% - #0: ToddCoxeter: diff 0.10.0 | +12,231,652 | +32,981,256 | -32.1% - #0: ToddCoxeter: phase 0.10 = 1.051s | run 0 = 7.617s | all runs = 7.617s | elapsed = 7.617s + #0: ToddCoxeter: HLT 0.10.1 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,750 | 11,773,835 | 31,163,585 + #0: ToddCoxeter: diff 0.10.0 | +11,303,227 | +489,785 | +11,793,012 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 38,786,740 | 38,772,260 | 50.0% + #0: ToddCoxeter: diff 0.10.0 | +12,231,652 | +32,981,256 | -32.1% + #0: ToddCoxeter: phase 0.10 = 829ms | run 0 = 5.955s | all runs = 5.955s | elapsed = 5.955s ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.11 START (lookahead_extent() = partial, lookahead_style() = hlt) #0: ToddCoxeter: LOOKAHEAD 0.11.0 | active | killed | defined #0: ToddCoxeter: nodes | 19,389,750 | 11,773,835 | 31,163,585 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 38,786,740 | 38,772,260 | 50.0% - #0: ToddCoxeter: time | run 0 = 7.617s | all runs = 7.617s | elapsed = 7.617s + #0: ToddCoxeter: time | run 0 = 5.955s | all runs = 5.955s | elapsed = 5.955s #0: ToddCoxeter: because a >= n #0: ToddCoxeter: where: a = number_of_nodes_active() = 19,389,750 #0: ToddCoxeter: n = lookahead_next() = 19,389,704 ++++++++++++++++++++++++++++++++ #1: ToddCoxeter: LOOKAHEAD 0.11.1 | active | killed | defined - #1: ToddCoxeter: nodes | 19,119,246 | 12,044,357 | 31,163,585 - #1: ToddCoxeter: diff 0.11.0 | -270,504 | +270,522 | +0 + #1: ToddCoxeter: nodes | 19,361,711 | 11,801,893 | 31,163,585 + #1: ToddCoxeter: diff 0.11.0 | -28,039 | +28,058 | +0 #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 38,564,145 | 37,912,839 | 50.4% - #1: ToddCoxeter: diff 0.11.0 | -222,595 | -859,421 | +0.4% - #1: ToddCoxeter: phase 0.11 = 385ms | run 0 = 8.002s | all runs = 8.002s | elapsed = 8.002s - #1: ToddCoxeter: lookahead progress | ~12.6% + #1: ToddCoxeter: edges | 38,761,553 | 38,685,291 | 50.0% + #1: ToddCoxeter: diff 0.11.0 | -25,187 | -86,969 | +0.0% + #1: ToddCoxeter: phase 0.11 = 46ms | run 0 = 6.002s | all runs = 6.002s | elapsed = 6.002s + #1: ToddCoxeter: lookahead progress | ~4.6% ++++++++++++++++++++++++++++++++ #1: ToddCoxeter: LOOKAHEAD 0.11.2 | active | killed | defined - #1: ToddCoxeter: nodes | 18,894,507 | 12,269,078 | 31,163,585 - #1: ToddCoxeter: diff 0.11.1 | -224,739 | +224,721 | +0 - #1: ToddCoxeter: diff 0.11.0 | -495,243 | +495,243 | +0 + #1: ToddCoxeter: nodes | 18,900,346 | 12,263,243 | 31,163,585 + #1: ToddCoxeter: diff 0.11.1 | -461,365 | +461,350 | +0 + #1: ToddCoxeter: diff 0.11.0 | -489,404 | +489,408 | +0 #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 38,371,598 | 37,206,430 | 50.8% - #1: ToddCoxeter: diff 0.11.1 | -192,547 | -706,409 | +0.3% - #1: ToddCoxeter: diff 0.11.0 | -415,142 | -1,565,830 | +0.8% - #1: ToddCoxeter: phase 0.11 = 1.385s | run 0 = 9.003s | all runs = 9.003s | elapsed = 9.003s - #1: ToddCoxeter: lookahead progress | ~38.8% - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.11.3 | active | killed | defined - #1: ToddCoxeter: nodes | 15,851,580 | 15,312,085 | 31,163,585 - #1: ToddCoxeter: diff 0.11.2 | -3,042,927 | +3,043,007 | +0 - #1: ToddCoxeter: diff 0.11.0 | -3,538,170 | +3,538,250 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 41,333,919 | 22,072,401 | 65.2% - #1: ToddCoxeter: diff 0.11.2 | +2,962,321 | -15,134,029 | +14.4% - #1: ToddCoxeter: diff 0.11.0 | +2,547,179 | -16,699,859 | +15.2% - #1: ToddCoxeter: phase 0.11 = 2.386s | run 0 = 10.003s | all runs = 10.003s | elapsed = 10.003s - #1: ToddCoxeter: lookahead progress | ~62.6% + #1: ToddCoxeter: edges | 38,376,840 | 37,224,544 | 50.8% + #1: ToddCoxeter: diff 0.11.1 | -384,713 | -1,460,747 | +0.7% + #1: ToddCoxeter: diff 0.11.0 | -409,900 | -1,547,716 | +0.8% + #1: ToddCoxeter: phase 0.11 = 1.047s | run 0 = 7.002s | all runs = 7.002s | elapsed = 7.002s + #1: ToddCoxeter: lookahead progress | ~38.4% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.11.3 | active | killed | defined + #1: ToddCoxeter: nodes | 14,438,129 | 16,725,554 | 31,163,585 + #1: ToddCoxeter: diff 0.11.2 | -4,462,217 | +4,462,311 | +0 + #1: ToddCoxeter: diff 0.11.0 | -4,951,621 | +4,951,719 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 42,716,669 | 15,035,847 | 74.0% + #1: ToddCoxeter: diff 0.11.2 | +4,339,829 | -22,188,697 | +23.2% + #1: ToddCoxeter: diff 0.11.0 | +3,929,929 | -23,736,413 | +24.0% + #1: ToddCoxeter: phase 0.11 = 2.047s | run 0 = 8.002s | all runs = 8.002s | elapsed = 8.002s + #1: ToddCoxeter: lookahead progress | ~72.2% ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.11 STOP - #0: ToddCoxeter: LOOKAHEAD 0.11.4 | active | killed | defined - #0: ToddCoxeter: nodes | 13,427,510 | 17,736,075 | 31,163,585 - #0: ToddCoxeter: diff 0.11.3 | -2,424,070 | +2,423,990 | +0 - #0: ToddCoxeter: diff 0.11.0 | -5,962,240 | +5,962,240 | +0 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 43,882,513 | 9,827,527 | 81.7% - #0: ToddCoxeter: diff 0.11.3 | +2,548,594 | -12,244,874 | +16.5% - #0: ToddCoxeter: diff 0.11.0 | +5,095,773 | -28,944,733 | +31.7% - #0: ToddCoxeter: phase 0.11 = 2.893s | run 0 = 10.511s | all runs = 10.511s | elapsed = 10.511s + #0: ToddCoxeter: LOOKAHEAD 0.11.4 | active | killed | defined + #0: ToddCoxeter: nodes | 13,427,510 | 17,736,075 | 31,163,585 + #0: ToddCoxeter: diff 0.11.3 | -1,010,619 | +1,010,521 | +0 + #0: ToddCoxeter: diff 0.11.0 | -5,962,240 | +5,962,240 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 43,882,513 | 9,827,527 | 81.7% + #0: ToddCoxeter: diff 0.11.3 | +1,165,844 | -5,208,320 | +7.7% + #0: ToddCoxeter: diff 0.11.0 | +5,095,773 | -28,944,733 | +31.7% + #0: ToddCoxeter: phase 0.11 = 2.208s | run 0 = 8.163s | all runs = 8.163s | elapsed = 8.163s #0: ToddCoxeter: lookahead_next() is now 19,389,704 (+0) #0: ToddCoxeter: because: #0: ToddCoxeter: 1. n <= f x a = 26,855,020 @@ -419,95 +397,84 @@ Running the above script produces the following output: #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.12 START - #0: ToddCoxeter: HLT 0.12.0 | active | killed | defined - #0: ToddCoxeter: nodes | 13,427,510 | 17,736,075 | 31,163,585 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 43,882,513 | 9,827,527 | 81.7% - #0: ToddCoxeter: time | run 0 = 10.511s | all runs = 10.511s | elapsed = 10.511s + #0: ToddCoxeter: HLT 0.12.0 | active | killed | defined + #0: ToddCoxeter: nodes | 13,427,510 | 17,736,075 | 31,163,585 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 43,882,513 | 9,827,527 | 81.7% + #0: ToddCoxeter: time | run 0 = 8.163s | all runs = 8.163s | elapsed = 8.163s ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.12 STOP - #0: ToddCoxeter: HLT 0.12.1 | active | killed | defined - #0: ToddCoxeter: nodes | 19,389,776 | 17,959,888 | 37,349,664 - #0: ToddCoxeter: diff 0.12.0 | +5,962,266 | +223,813 | +6,186,079 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 50,324,580 | 27,234,524 | 64.9% - #0: ToddCoxeter: diff 0.12.0 | +6,442,067 | +17,406,997 | -16.8% - #0: ToddCoxeter: phase 0.12 = 267ms | run 0 = 10.778s | all runs = 10.778s | elapsed = 10.779s + #0: ToddCoxeter: HLT 0.12.1 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,776 | 17,959,888 | 37,349,664 + #0: ToddCoxeter: diff 0.12.0 | +5,962,266 | +223,813 | +6,186,079 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 50,324,580 | 27,234,524 | 64.9% + #0: ToddCoxeter: diff 0.12.0 | +6,442,067 | +17,406,997 | -16.8% + #0: ToddCoxeter: phase 0.12 = 230ms | run 0 = 8.393s | all runs = 8.393s | elapsed = 8.393s ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.13 START (lookahead_extent() = partial, lookahead_style() = hlt) - #0: ToddCoxeter: LOOKAHEAD 0.13.0 | active | killed | defined - #0: ToddCoxeter: nodes | 19,389,776 | 17,959,888 | 37,349,664 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 50,324,580 | 27,234,524 | 64.9% - #0: ToddCoxeter: time | run 0 = 10.778s | all runs = 10.778s | elapsed = 10.779s + #0: ToddCoxeter: LOOKAHEAD 0.13.0 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,776 | 17,959,888 | 37,349,664 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 50,324,580 | 27,234,524 | 64.9% + #0: ToddCoxeter: time | run 0 = 8.393s | all runs = 8.393s | elapsed = 8.393s #0: ToddCoxeter: because a >= n #0: ToddCoxeter: where: a = number_of_nodes_active() = 19,389,776 #0: ToddCoxeter: n = lookahead_next() = 19,389,704 ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.13.1 | active | killed | defined - #1: ToddCoxeter: nodes | 19,314,200 | 18,035,464 | 37,349,664 - #1: ToddCoxeter: diff 0.13.0 | -75,576 | +75,576 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 50,245,486 | 27,011,314 | 65.0% - #1: ToddCoxeter: diff 0.13.0 | -79,094 | -223,210 | +0.2% - #1: ToddCoxeter: phase 0.13 = 224ms | run 0 = 11.003s | all runs = 11.003s | elapsed = 11.003s - #1: ToddCoxeter: lookahead progress | ~9.0% + #1: ToddCoxeter: LOOKAHEAD 0.13.1 | active | killed | defined + #1: ToddCoxeter: nodes | 19,186,302 | 18,163,362 | 37,349,664 + #1: ToddCoxeter: diff 0.13.0 | -203,474 | +203,474 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 50,106,203 | 26,639,005 | 65.3% + #1: ToddCoxeter: diff 0.13.0 | -218,377 | -595,519 | +0.4% + #1: ToddCoxeter: phase 0.13 = 609ms | run 0 = 9.002s | all runs = 9.002s | elapsed = 9.002s + #1: ToddCoxeter: lookahead progress | ~20.7% ++++++++++++++++++++++++++++++++ #1: ToddCoxeter: LOOKAHEAD 0.13.2 | active | killed | defined - #1: ToddCoxeter: nodes | 19,102,330 | 18,247,350 | 37,349,664 - #1: ToddCoxeter: diff 0.13.1 | -211,870 | +211,886 | +0 - #1: ToddCoxeter: diff 0.13.0 | -287,446 | +287,462 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 50,032,914 | 26,376,406 | 65.5% - #1: ToddCoxeter: diff 0.13.1 | -212,572 | -634,908 | +0.4% - #1: ToddCoxeter: diff 0.13.0 | -291,666 | -858,118 | +0.6% - #1: ToddCoxeter: phase 0.13 = 1.225s | run 0 = 12.003s | all runs = 12.003s | elapsed = 12.003s - #1: ToddCoxeter: lookahead progress | ~31.3% - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.13.3 | active | killed | defined - #1: ToddCoxeter: nodes | 18,872,056 | 18,477,610 | 37,349,664 - #1: ToddCoxeter: diff 0.13.2 | -230,274 | +230,260 | +0 - #1: ToddCoxeter: diff 0.13.0 | -517,720 | +517,722 | +0 + #1: ToddCoxeter: nodes | 18,905,330 | 18,444,334 | 37,349,664 + #1: ToddCoxeter: diff 0.13.1 | -280,972 | +280,972 | +0 + #1: ToddCoxeter: diff 0.13.0 | -484,446 | +484,446 | +0 #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 49,788,690 | 25,699,534 | 66.0% - #1: ToddCoxeter: diff 0.13.2 | -244,224 | -676,872 | +0.5% - #1: ToddCoxeter: diff 0.13.0 | -535,890 | -1,534,990 | +1.1% - #1: ToddCoxeter: phase 0.13 = 2.225s | run 0 = 13.004s | all runs = 13.004s | elapsed = 13.004s - #1: ToddCoxeter: lookahead progress | ~58.4% + #1: ToddCoxeter: edges | 49,829,308 | 25,792,012 | 65.9% + #1: ToddCoxeter: diff 0.13.1 | -276,895 | -846,993 | +0.6% + #1: ToddCoxeter: diff 0.13.0 | -495,272 | -1,442,512 | +1.0% + #1: ToddCoxeter: phase 0.13 = 1.610s | run 0 = 10.003s | all runs = 10.003s | elapsed = 10.003s + #1: ToddCoxeter: lookahead progress | ~54.1% #0: ToddCoxeter: large collapse, number of coincidences 100,000 >= 100,000 = large_collapse()! ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.13.4 | active | killed | defined - #1: ToddCoxeter: nodes | 12,447,893 | 24,901,915 | 37,349,664 - #1: ToddCoxeter: diff 0.13.3 | -6,424,163 | +6,424,305 | +0 - #1: ToddCoxeter: diff 0.13.0 | -6,941,883 | +6,942,027 | +0 + #1: ToddCoxeter: LOOKAHEAD 0.13.3 | active | killed | defined + #1: ToddCoxeter: nodes | 11,154,426 | 26,195,391 | 37,349,664 + #1: ToddCoxeter: diff 0.13.2 | -7,750,904 | +7,751,057 | +0 + #1: ToddCoxeter: diff 0.13.0 | -8,235,350 | +8,235,503 | +0 #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 0 | 49,791,572 | 0.0% - #1: ToddCoxeter: diff 0.13.3 | -49,788,690 | +24,092,038 | -66.0% - #1: ToddCoxeter: diff 0.13.0 | -50,324,580 | +22,557,048 | -64.9% - #1: ToddCoxeter: phase 0.13 = 3.225s | run 0 = 14.004s | all runs = 14.004s | elapsed = 14.004s + #1: ToddCoxeter: edges | 0 | 44,617,704 | 0.0% + #1: ToddCoxeter: diff 0.13.2 | -49,829,308 | +18,825,692 | -65.9% + #1: ToddCoxeter: diff 0.13.0 | -50,324,580 | +17,383,180 | -64.9% + #1: ToddCoxeter: phase 0.13 = 2.610s | run 0 = 11.003s | all runs = 11.003s | elapsed = 11.003s #1: ToddCoxeter: lookahead progress | ~66.6% ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.13.5 | active | killed | defined - #1: ToddCoxeter: nodes | 5,024,869 | 32,324,910 | 37,349,664 - #1: ToddCoxeter: diff 0.13.4 | -7,423,024 | +7,422,995 | +0 - #1: ToddCoxeter: diff 0.13.0 | -14,364,907 | +14,365,022 | +0 + #1: ToddCoxeter: LOOKAHEAD 0.13.4 | active | killed | defined + #1: ToddCoxeter: nodes | 2,148,036 | 35,201,729 | 37,349,664 + #1: ToddCoxeter: diff 0.13.3 | -9,006,390 | +9,006,338 | +0 + #1: ToddCoxeter: diff 0.13.0 | -17,241,740 | +17,241,841 | +0 #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 0 | 20,099,476 | 0.0% - #1: ToddCoxeter: diff 0.13.4 | +0 | -29,692,096 | +0.0% - #1: ToddCoxeter: diff 0.13.0 | -50,324,580 | -7,135,048 | -64.9% - #1: ToddCoxeter: phase 0.13 = 4.226s | run 0 = 15.004s | all runs = 15.004s | elapsed = 15.004s + #1: ToddCoxeter: edges | 0 | 8,592,144 | 0.0% + #1: ToddCoxeter: diff 0.13.3 | +0 | -36,025,560 | +0.0% + #1: ToddCoxeter: diff 0.13.0 | -50,324,580 | -18,642,380 | -64.9% + #1: ToddCoxeter: phase 0.13 = 3.610s | run 0 = 12.003s | all runs = 12.003s | elapsed = 12.003s #1: ToddCoxeter: lookahead progress | ~66.6% ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: LOOKAHEAD 0.13 STOP - #0: ToddCoxeter: LOOKAHEAD 0.13.6 | active | killed | defined + #0: ToddCoxeter: LOOKAHEAD 0.13.5 | active | killed | defined #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 - #0: ToddCoxeter: diff 0.13.5 | -4,581,349 | +4,581,234 | +0 + #0: ToddCoxeter: diff 0.13.4 | -1,704,516 | +1,704,415 | +0 #0: ToddCoxeter: diff 0.13.0 | -18,946,256 | +18,946,256 | +0 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% - #0: ToddCoxeter: diff 0.13.5 | +1,774,080 | -20,099,476 | +100.0% + #0: ToddCoxeter: diff 0.13.4 | +1,774,080 | -8,592,144 | +100.0% #0: ToddCoxeter: diff 0.13.0 | -48,550,500 | -27,234,524 | +35.1% - #0: ToddCoxeter: phase 0.13 = 5.080s | run 0 = 15.858s | all runs = 15.858s | elapsed = 15.858s + #0: ToddCoxeter: phase 0.13 = 3.928s | run 0 = 12.321s | all runs = 12.321s | elapsed = 12.321s #0: ToddCoxeter: lookahead_next() is now max(f x a = 887,040, m = 10,000) (-18,502,664) #0: ToddCoxeter: because f x a < n #0: ToddCoxeter: where: a = number_of_nodes_active() = 443,520 @@ -520,42 +487,32 @@ Running the above script produces the following output: #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% - #0: ToddCoxeter: time | run 0 = 15.858s | all runs = 15.858s | elapsed = 15.858s - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: HLT 0.14.1 | active | killed | defined - #1: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 - #1: ToddCoxeter: diff 0.14.0 | +0 | +0 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% - #1: ToddCoxeter: diff 0.14.0 | +0 | +0 | +0.0% - #1: ToddCoxeter: phase 0.14 = 146ms | run 0 = 16.004s | all runs = 16.004s | elapsed = 16.005s + #0: ToddCoxeter: time | run 0 = 12.321s | all runs = 12.321s | elapsed = 12.321s ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: HLT 0.14 STOP - #0: ToddCoxeter: HLT 0.14.2 | active | killed | defined + #0: ToddCoxeter: HLT 0.14.1 | active | killed | defined #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 - #0: ToddCoxeter: diff 0.14.1 | +0 | +0 | +0 #0: ToddCoxeter: diff 0.14.0 | +0 | +0 | +0 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% - #0: ToddCoxeter: diff 0.14.1 | +0 | +0 | +0.0% #0: ToddCoxeter: diff 0.14.0 | +0 | +0 | +0.0% - #0: ToddCoxeter: phase 0.14 = 151ms | run 0 = 16.009s | all runs = 16.009s | elapsed = 16.010s + #0: ToddCoxeter: phase 0.14 = 108ms | run 0 = 12.430s | all runs = 12.430s | elapsed = 12.430s ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.15.3 | active | killed | defined + #0: ToddCoxeter: HLT 0.15.2 | active | killed | defined #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 - #0: ToddCoxeter: diff 0.15.2 | +0 | +0 | +0 + #0: ToddCoxeter: diff 0.15.1 | +0 | +0 | +0 #0: ToddCoxeter: diff 0.15.0 | +0 | +0 | +0 #0: ToddCoxeter: | active | missing | % complete #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% - #0: ToddCoxeter: diff 0.15.2 | +0 | +0 | +0.0% + #0: ToddCoxeter: diff 0.15.1 | +0 | +0 | +0.0% #0: ToddCoxeter: diff 0.15.0 | +0 | +0 | +0.0% - #0: ToddCoxeter: phase 0.15 = 151ms | run 0 = 16.010s | all runs = 16.010s | elapsed = 16.010s + #0: ToddCoxeter: phase 0.15 = 108ms | run 0 = 12.430s | all runs = 12.430s | elapsed = 12.430s ++++++++++++++++++++++++++++++++ #0: ToddCoxeter: RUN 0 STOP (finished) #0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch #0: ToddCoxeter: num. phases | 7 | 0 | 8 | 0 - #0: ToddCoxeter: time spent in phases | 13.184s (82%) | - (0%) | 2.826s (18%) | - (0%) - #0: ToddCoxeter: phase 0.15 = 160ms | run 0 = 16.019s | all runs = 16.019s | elapsed = 16.019s + #0: ToddCoxeter: time spent in phases | 10.163s (82%) | - (0%) | 2.267s (18%) | - (0%) + #0: ToddCoxeter: phase 0.15 = 114ms | run 0 = 12.436s | all runs = 12.436s | elapsed = 12.436s ``` :simple-ticktick: The computed size of the group matches the size of the group From ade15a7c75dd89e5cc59f17d9cedd38e731f10fd Mon Sep 17 00:00:00 2001 From: Joseph Edwards Date: Tue, 2 Jun 2026 13:07:30 +0100 Subject: [PATCH 6/7] Add ACE tabs --- docs/examples/atlas/mathieu/m11.md | 136 ++-- docs/examples/atlas/mathieu/m12.md | 222 +++--- docs/examples/atlas/mathieu/m22.md | 1006 ++++++++++++++-------------- mkdocs.yml | 1 + 4 files changed, 704 insertions(+), 661 deletions(-) diff --git a/docs/examples/atlas/mathieu/m11.md b/docs/examples/atlas/mathieu/m11.md index b7a7eeb..cfd7a84 100644 --- a/docs/examples/atlas/mathieu/m11.md +++ b/docs/examples/atlas/mathieu/m11.md @@ -2,80 +2,93 @@ > Order: $7,920$ -> Presentation: $\langle{ a, b \mid a^2 = b^4 = (ab)^{11} = (ab^2)^6 = ababab^{−1}abab^2ab^{−1}abab^{−1}ab^{−1} = 1 }\rangle$ +> Presentation: +> $\langle{ a, b \mid a^2 = b^4 = (ab)^{11} = (ab^2)^6 = ababab^{−1}abab^2ab^{−1}abab^{−1}ab^{−1} = 1 }\rangle$ On this page, we verify that the above claimed presentation of the Mathieu group M~11~ defines a group of order $7,920$. ## The code -In [libsemigroups_pybind11][], the following script constructs the presentation -for M~11~ and runs the Todd-Coxeter algorithm. +=== "Python" -```python -from libsemigroups_pybind11 import Presentation, ToddCoxeter, congruence_kind, presentation -from libsemigroups_pybind11.words import parse_relations + In [libsemigroups_pybind11][], the following script constructs the + presentation for M~11~ and runs the Todd-Coxeter algorithm. -# Setup the presentation object with the empty and inverses, so it can represent a group -p = Presentation("abAB") -p.contains_empty_word(True) -presentation.add_inverse_rules(p, "ABab") + ```python + from libsemigroups_pybind11 import Presentation, ToddCoxeter, congruence_kind, presentation + from libsemigroups_pybind11.words import parse_relations -# Add the defining relations -presentation.add_rule(p, parse_relations("a^2"), "") -presentation.add_rule(p, parse_relations("b^4"), "") -presentation.add_rule(p, parse_relations("(ab)^11"), "") -presentation.add_rule(p, parse_relations("(ab^2)^6"), "") -presentation.add_rule(p, parse_relations("ababaBabab^2aBabaBaB"), "") + # Setup the presentation object with the empty and inverses, so it can represent a group + p = Presentation("abAB") + p.contains_empty_word(True) + presentation.add_inverse_rules(p, "ABab") -# Run the Todd-Coxeter algorithm -tc = ToddCoxeter(congruence_kind.twosided, p) -tc.run() + # Add the defining relations + presentation.add_rule(p, parse_relations("a^2"), "") + presentation.add_rule(p, parse_relations("b^4"), "") + presentation.add_rule(p, parse_relations("(ab)^11"), "") + presentation.add_rule(p, parse_relations("(ab^2)^6"), "") + presentation.add_rule(p, parse_relations("ababaBabab^2aBabaBaB"), "") -assert tc.number_of_classes() == 7920 -``` + # Run the Todd-Coxeter algorithm + tc = ToddCoxeter(congruence_kind.twosided, p) + tc.run() + + assert tc.number_of_classes() == 7920 + ``` + +=== "ACE" + + Coming soon! ## The output -Running the above script produces the following output: - -``` -++++++++++++++++++++++++++++++++ -#0: ToddCoxeter: RUN 0 START (strategy() = hlt) -#0: ToddCoxeter: |A| = 4, |R| = 9, |u| + |v| ∈ [2, 22], ∑(|u| + |v|) = 73 -++++++++++++++++++++++++++++++++ -#0: ToddCoxeter: HLT 0.0 START -#0: ToddCoxeter: HLT 0.0.0 | active | killed | defined -#0: ToddCoxeter: nodes | 1 | 0 | 1 -#0: ToddCoxeter: | active | missing | % complete -#0: ToddCoxeter: edges | 0 | 4 | 0.0% -#0: ToddCoxeter: time | run 0 = 28µs | all runs = 28µs | elapsed = 92µs -++++++++++++++++++++++++++++++++ -#0: ToddCoxeter: HLT 0.0 STOP -#0: ToddCoxeter: HLT 0.0.1 | active | killed | defined -#0: ToddCoxeter: nodes | 7,920 | 1,992,427 | 2,000,347 -#0: ToddCoxeter: diff 0.0.0 | +7,919 | +1,992,427 | +2,000,346 -#0: ToddCoxeter: | active | missing | % complete -#0: ToddCoxeter: edges | 31,680 | 0 | 100.0% -#0: ToddCoxeter: diff 0.0.0 | +31,680 | -4 | +100.0% -#0: ToddCoxeter: phase 0.0 = 176ms | run 0 = 176ms | all runs = 176ms | elapsed = 176ms -++++++++++++++++++++++++++++++++ -#0: ToddCoxeter: HLT 0.1.2 | active | killed | defined -#0: ToddCoxeter: nodes | 7,920 | 1,992,427 | 2,000,347 -#0: ToddCoxeter: diff 0.1.1 | +0 | +0 | +0 -#0: ToddCoxeter: diff 0.1.0 | +7,919 | +1,992,427 | +2,000,346 -#0: ToddCoxeter: | active | missing | % complete -#0: ToddCoxeter: edges | 31,680 | 0 | 100.0% -#0: ToddCoxeter: diff 0.1.1 | +0 | +0 | +0.0% -#0: ToddCoxeter: diff 0.1.0 | +31,680 | -4 | +100.0% -#0: ToddCoxeter: phase 0.1 = 176ms | run 0 = 176ms | all runs = 176ms | elapsed = 176ms -++++++++++++++++++++++++++++++++ -#0: ToddCoxeter: RUN 0 STOP (finished) -#0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch -#0: ToddCoxeter: num. phases | 0 | 0 | 1 | 0 -#0: ToddCoxeter: time spent in phases | - (0%) | - (0%) | 176ms (100%) | - (0%) -#0: ToddCoxeter: phase 0.1 = 176ms | run 0 = 176ms | all runs = 176ms | elapsed = 176ms -``` +=== "Python" + + Running the above Python script produces the following output: + + ``` + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 START (strategy() = hlt) + #0: ToddCoxeter: |A| = 4, |R| = 9, |u| + |v| ∈ [2, 22], ∑(|u| + |v|) = 73 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 START + #0: ToddCoxeter: HLT 0.0.0 | active | killed | defined + #0: ToddCoxeter: nodes | 1 | 0 | 1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 0 | 4 | 0.0% + #0: ToddCoxeter: time | run 0 = 28µs | all runs = 28µs | elapsed = 92µs + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 STOP + #0: ToddCoxeter: HLT 0.0.1 | active | killed | defined + #0: ToddCoxeter: nodes | 7,920 | 1,992,427 | 2,000,347 + #0: ToddCoxeter: diff 0.0.0 | +7,919 | +1,992,427 | +2,000,346 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 31,680 | 0 | 100.0% + #0: ToddCoxeter: diff 0.0.0 | +31,680 | -4 | +100.0% + #0: ToddCoxeter: phase 0.0 = 176ms | run 0 = 176ms | all runs = 176ms | elapsed = 176ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.1.2 | active | killed | defined + #0: ToddCoxeter: nodes | 7,920 | 1,992,427 | 2,000,347 + #0: ToddCoxeter: diff 0.1.1 | +0 | +0 | +0 + #0: ToddCoxeter: diff 0.1.0 | +7,919 | +1,992,427 | +2,000,346 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 31,680 | 0 | 100.0% + #0: ToddCoxeter: diff 0.1.1 | +0 | +0 | +0.0% + #0: ToddCoxeter: diff 0.1.0 | +31,680 | -4 | +100.0% + #0: ToddCoxeter: phase 0.1 = 176ms | run 0 = 176ms | all runs = 176ms | elapsed = 176ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 STOP (finished) + #0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch + #0: ToddCoxeter: num. phases | 0 | 0 | 1 | 0 + #0: ToddCoxeter: time spent in phases | - (0%) | - (0%) | 176ms (100%) | - (0%) + #0: ToddCoxeter: phase 0.1 = 176ms | run 0 = 176ms | all runs = 176ms | elapsed = 176ms + ``` + +=== "ACE" + + Coming soon! :simple-ticktick: The computed size of the group matches the size of the group provided on [the ATLAS][atlas]: $7,920$. @@ -88,4 +101,5 @@ provided on [the ATLAS][atlas]: $7,920$. the same as above. [atlas]: https://brauer.maths.qmul.ac.uk/Atlas/v3/spor/ -[libsemigroups_pybind11]: https://libsemigroups.github.io/libsemigroups_pybind11/index.html +[libsemigroups_pybind11]: + https://libsemigroups.github.io/libsemigroups_pybind11/index.html diff --git a/docs/examples/atlas/mathieu/m12.md b/docs/examples/atlas/mathieu/m12.md index 9235cb5..999046f 100644 --- a/docs/examples/atlas/mathieu/m12.md +++ b/docs/examples/atlas/mathieu/m12.md @@ -2,128 +2,142 @@ > Order: $95,040$ -> Presentation: $\langle{ a, b \mid a^2 = b^3 = (ab)^{11} = [a, b]^6 = (ababab^{−1})^6 = 1 }\rangle$ +> Presentation: +> $\langle{ a, b \mid a^2 = b^3 = (ab)^{11} = [a, b]^6 = (ababab^{−1})^6 = 1 }\rangle$ On this page, we verify that the above claimed presentation of the Mathieu group M~12~ defines a group of order $95,040$. ## The code -In [libsemigroups_pybind11][], the following script constructs the presentation -for M~12~ and runs the Todd-Coxeter algorithm. +=== "Python" -```python -from libsemigroups_pybind11 import Presentation, ToddCoxeter, congruence_kind, presentation -from libsemigroups_pybind11.words import parse_relations + In [libsemigroups_pybind11][], the following script constructs the + presentation for M~12~ and runs the Todd-Coxeter algorithm. -# Setup the presentation object with the empty and inverses, so it can represent a group -p = Presentation("abAB") -p.contains_empty_word(True) -presentation.add_inverse_rules(p, "ABab") + ```python + from libsemigroups_pybind11 import Presentation, ToddCoxeter, congruence_kind, presentation + from libsemigroups_pybind11.words import parse_relations -# Add the defining relations -presentation.add_rule(p, parse_relations("a^2"), "") -presentation.add_rule(p, parse_relations("b^3"), "") -presentation.add_rule(p, parse_relations("(ab)^11"), "") -presentation.add_rule(p, parse_relations("(a,b)^6"), "") -presentation.add_rule(p, parse_relations("(ababaB)^6"), "") + # Setup the presentation object with the empty and inverses, so it can represent a group + p = Presentation("abAB") + p.contains_empty_word(True) + presentation.add_inverse_rules(p, "ABab") + # Add the defining relations + presentation.add_rule(p, parse_relations("a^2"), "") + presentation.add_rule(p, parse_relations("b^3"), "") + presentation.add_rule(p, parse_relations("(ab)^11"), "") + presentation.add_rule(p, parse_relations("(a,b)^6"), "") + presentation.add_rule(p, parse_relations("(ababaB)^6"), "") -# Run the Todd-Coxeter algorithm -tc = ToddCoxeter(congruence_kind.twosided, p) -tc.run() -assert tc.number_of_classes() == 95040 -``` + # Run the Todd-Coxeter algorithm + tc = ToddCoxeter(congruence_kind.twosided, p) + tc.run() -## The output + assert tc.number_of_classes() == 95040 + ``` -Running the above script produces the following output: +=== "ACE" -??? info "Output from the Python script" + Coming soon! - ``` - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: RUN 0 START (strategy() = hlt) - #0: ToddCoxeter: |A| = 4, |R| = 9, |u| + |v| ∈ [2, 36], ∑(|u| + |v|) = 95 - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.0 START - #0: ToddCoxeter: HLT 0.0.0 | active | killed | defined - #0: ToddCoxeter: nodes | 1 | 0 | 1 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 0 | 4 | 0.0% - #0: ToddCoxeter: time | run 0 = 24µs | all runs = 24µs | elapsed = 84µs - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.0 STOP - #0: ToddCoxeter: HLT 0.0.1 | active | killed | defined - #0: ToddCoxeter: nodes | 5,000,004 | 2,964,327 | 7,964,331 - #0: ToddCoxeter: diff 0.0.0 | +5,000,003 | +2,964,327 | +7,964,330 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 5,782,533 | 14,217,483 | 28.9% - #0: ToddCoxeter: diff 0.0.0 | +5,782,533 | +14,217,479 | +28.9% - #0: ToddCoxeter: phase 0.0 = 489ms | run 0 = 489ms | all runs = 489ms | elapsed = 489ms - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.1 START (lookahead_extent() = partial, lookahead_style() = hlt) - #0: ToddCoxeter: LOOKAHEAD 0.1.0 | active | killed | defined - #0: ToddCoxeter: nodes | 5,000,004 | 2,964,327 | 7,964,331 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 5,782,533 | 14,217,483 | 28.9% - #0: ToddCoxeter: time | run 0 = 489ms | all runs = 489ms | elapsed = 489ms - #0: ToddCoxeter: because a >= n - #0: ToddCoxeter: where: a = number_of_nodes_active() = 5,000,004 - #0: ToddCoxeter: n = lookahead_next() = 5,000,000 - #0: ToddCoxeter: large collapse, number of coincidences 100,002 >= 100,000 = large_collapse()! - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.1 STOP - #0: ToddCoxeter: LOOKAHEAD 0.1.1 | active | killed | defined - #0: ToddCoxeter: nodes | 95,046 | 7,869,285 | 7,964,331 - #0: ToddCoxeter: diff 0.1.0 | -4,904,958 | +4,904,958 | +0 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 380,177 | 7 | 100.0% - #0: ToddCoxeter: diff 0.1.0 | -5,402,356 | -14,217,476 | +71.1% - #0: ToddCoxeter: phase 0.1 = 449ms | run 0 = 939ms | all runs = 939ms | elapsed = 939ms - #0: ToddCoxeter: lookahead_next() is now max(f x a = 190,092, m = 10,000) (-4,809,908) - #0: ToddCoxeter: because f x a < n - #0: ToddCoxeter: where: a = number_of_nodes_active() = 95,046 - #0: ToddCoxeter: f = lookahead_growth_factor() = 2 - #0: ToddCoxeter: m = lookahead_min() = 10,000 - #0: ToddCoxeter: n = lookahead_next() = 5,000,000 - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.2 START - #0: ToddCoxeter: HLT 0.2.0 | active | killed | defined - #0: ToddCoxeter: nodes | 95,046 | 7,869,285 | 7,964,331 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 380,177 | 7 | 100.0% - #0: ToddCoxeter: time | run 0 = 939ms | all runs = 939ms | elapsed = 939ms - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.2 STOP - #0: ToddCoxeter: HLT 0.2.1 | active | killed | defined - #0: ToddCoxeter: nodes | 95,040 | 7,869,292 | 7,964,332 - #0: ToddCoxeter: diff 0.2.0 | -6 | +7 | +1 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 380,160 | 0 | 100.0% - #0: ToddCoxeter: diff 0.2.0 | -17 | -7 | +0.0% - #0: ToddCoxeter: phase 0.2 = 13ms | run 0 = 952ms | all runs = 952ms | elapsed = 952ms - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.3.2 | active | killed | defined - #0: ToddCoxeter: nodes | 95,040 | 7,869,292 | 7,964,332 - #0: ToddCoxeter: diff 0.3.1 | +0 | +0 | +0 - #0: ToddCoxeter: diff 0.3.0 | -6 | +7 | +1 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 380,160 | 0 | 100.0% - #0: ToddCoxeter: diff 0.3.1 | +0 | +0 | +0.0% - #0: ToddCoxeter: diff 0.3.0 | -17 | -7 | +0.0% - #0: ToddCoxeter: phase 0.3 = 13ms | run 0 = 952ms | all runs = 952ms | elapsed = 952ms - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: RUN 0 STOP (finished) - #0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch - #0: ToddCoxeter: num. phases | 1 | 0 | 2 | 0 - #0: ToddCoxeter: time spent in phases | 449ms (47%) | - (0%) | 502ms (53%) | - (0%) - #0: ToddCoxeter: phase 0.3 = 14ms | run 0 = 953ms | all runs = 953ms | elapsed = 953ms - ``` +## The output + +=== "Python" + + Running the above script produces the following output: + + ??? info "Output from the Python script" + + ``` + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 START (strategy() = hlt) + #0: ToddCoxeter: |A| = 4, |R| = 9, |u| + |v| ∈ [2, 36], ∑(|u| + |v|) = 95 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 START + #0: ToddCoxeter: HLT 0.0.0 | active | killed | defined + #0: ToddCoxeter: nodes | 1 | 0 | 1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 0 | 4 | 0.0% + #0: ToddCoxeter: time | run 0 = 24µs | all runs = 24µs | elapsed = 84µs + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 STOP + #0: ToddCoxeter: HLT 0.0.1 | active | killed | defined + #0: ToddCoxeter: nodes | 5,000,004 | 2,964,327 | 7,964,331 + #0: ToddCoxeter: diff 0.0.0 | +5,000,003 | +2,964,327 | +7,964,330 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 5,782,533 | 14,217,483 | 28.9% + #0: ToddCoxeter: diff 0.0.0 | +5,782,533 | +14,217,479 | +28.9% + #0: ToddCoxeter: phase 0.0 = 489ms | run 0 = 489ms | all runs = 489ms | elapsed = 489ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.1 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.1.0 | active | killed | defined + #0: ToddCoxeter: nodes | 5,000,004 | 2,964,327 | 7,964,331 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 5,782,533 | 14,217,483 | 28.9% + #0: ToddCoxeter: time | run 0 = 489ms | all runs = 489ms | elapsed = 489ms + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 5,000,004 + #0: ToddCoxeter: n = lookahead_next() = 5,000,000 + #0: ToddCoxeter: large collapse, number of coincidences 100,002 >= 100,000 = large_collapse()! + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.1 STOP + #0: ToddCoxeter: LOOKAHEAD 0.1.1 | active | killed | defined + #0: ToddCoxeter: nodes | 95,046 | 7,869,285 | 7,964,331 + #0: ToddCoxeter: diff 0.1.0 | -4,904,958 | +4,904,958 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,177 | 7 | 100.0% + #0: ToddCoxeter: diff 0.1.0 | -5,402,356 | -14,217,476 | +71.1% + #0: ToddCoxeter: phase 0.1 = 449ms | run 0 = 939ms | all runs = 939ms | elapsed = 939ms + #0: ToddCoxeter: lookahead_next() is now max(f x a = 190,092, m = 10,000) (-4,809,908) + #0: ToddCoxeter: because f x a < n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 95,046 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: m = lookahead_min() = 10,000 + #0: ToddCoxeter: n = lookahead_next() = 5,000,000 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.2 START + #0: ToddCoxeter: HLT 0.2.0 | active | killed | defined + #0: ToddCoxeter: nodes | 95,046 | 7,869,285 | 7,964,331 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,177 | 7 | 100.0% + #0: ToddCoxeter: time | run 0 = 939ms | all runs = 939ms | elapsed = 939ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.2 STOP + #0: ToddCoxeter: HLT 0.2.1 | active | killed | defined + #0: ToddCoxeter: nodes | 95,040 | 7,869,292 | 7,964,332 + #0: ToddCoxeter: diff 0.2.0 | -6 | +7 | +1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,160 | 0 | 100.0% + #0: ToddCoxeter: diff 0.2.0 | -17 | -7 | +0.0% + #0: ToddCoxeter: phase 0.2 = 13ms | run 0 = 952ms | all runs = 952ms | elapsed = 952ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.3.2 | active | killed | defined + #0: ToddCoxeter: nodes | 95,040 | 7,869,292 | 7,964,332 + #0: ToddCoxeter: diff 0.3.1 | +0 | +0 | +0 + #0: ToddCoxeter: diff 0.3.0 | -6 | +7 | +1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,160 | 0 | 100.0% + #0: ToddCoxeter: diff 0.3.1 | +0 | +0 | +0.0% + #0: ToddCoxeter: diff 0.3.0 | -17 | -7 | +0.0% + #0: ToddCoxeter: phase 0.3 = 13ms | run 0 = 952ms | all runs = 952ms | elapsed = 952ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 STOP (finished) + #0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch + #0: ToddCoxeter: num. phases | 1 | 0 | 2 | 0 + #0: ToddCoxeter: time spent in phases | 449ms (47%) | - (0%) | 502ms (53%) | - (0%) + #0: ToddCoxeter: phase 0.3 = 14ms | run 0 = 953ms | all runs = 953ms | elapsed = 953ms + ``` + +=== "ACE" + + Coming soon! :simple-ticktick: The computed size of the group matches the size of the group provided on [the ATLAS][atlas]: $95,040$. [atlas]: https://brauer.maths.qmul.ac.uk/Atlas/v3/spor/ -[libsemigroups_pybind11]: https://libsemigroups.github.io/libsemigroups_pybind11/index.html +[libsemigroups_pybind11]: + https://libsemigroups.github.io/libsemigroups_pybind11/index.html diff --git a/docs/examples/atlas/mathieu/m22.md b/docs/examples/atlas/mathieu/m22.md index 6d9422a..160309e 100644 --- a/docs/examples/atlas/mathieu/m22.md +++ b/docs/examples/atlas/mathieu/m22.md @@ -2,521 +2,535 @@ > Order: $443,520$ -> Presentation: $\langle{ a, b \mid a^2 = b^4 = (ab)^{11} = (ab^2)^5 = [a,bab]^3 = (ababab^{−1})^5 = 1 }\rangle$ +> Presentation: +> $\langle{ a, b \mid a^2 = b^4 = (ab)^{11} = (ab^2)^5 = [a,bab]^3 = (ababab^{−1})^5 = 1 }\rangle$ On this page, we verify that the above claimed presentation of the Mathieu group M~22~ defines a group of order $443,520$. ## The code -In [libsemigroups_pybind11][], the following script constructs the presentation -for M~11~ and runs the Todd-Coxeter algorithm. +=== "Python" -```python -from libsemigroups_pybind11 import Presentation, ToddCoxeter, congruence_kind, presentation -from libsemigroups_pybind11.words import parse_relations + In [libsemigroups_pybind11][], the following script constructs the presentation + for M~11~ and runs the Todd-Coxeter algorithm. -# Setup the presentation object with the empty and inverses, so it can represent a group -p = Presentation("abAB") -p.contains_empty_word(True) -presentation.add_inverse_rules(p, "ABab") + ```python + from libsemigroups_pybind11 import Presentation, ToddCoxeter, congruence_kind, presentation + from libsemigroups_pybind11.words import parse_relations -# Add the defining relations -presentation.add_rule(p, parse_relations("a^2"), "") -presentation.add_rule(p, parse_relations("b^4"), "") -presentation.add_rule(p, parse_relations("(ab)^11"), "") -presentation.add_rule(p, parse_relations("(ab^2)^5"), "") -presentation.add_rule(p, parse_relations("(a,bab)^3"), "") -presentation.add_rule(p, parse_relations("(ababaB)^5"), "") + # Setup the presentation object with the empty and inverses, so it can represent a group + p = Presentation("abAB") + p.contains_empty_word(True) + presentation.add_inverse_rules(p, "ABab") + # Add the defining relations + presentation.add_rule(p, parse_relations("a^2"), "") + presentation.add_rule(p, parse_relations("b^4"), "") + presentation.add_rule(p, parse_relations("(ab)^11"), "") + presentation.add_rule(p, parse_relations("(ab^2)^5"), "") + presentation.add_rule(p, parse_relations("(a,bab)^3"), "") + presentation.add_rule(p, parse_relations("(ababaB)^5"), "") -# Run the Todd-Coxeter algorithm -tc = ToddCoxeter(congruence_kind.twosided, p) -tc.run() -assert tc.number_of_classes() == 443520 -``` + # Run the Todd-Coxeter algorithm + tc = ToddCoxeter(congruence_kind.twosided, p) + tc.run() + + assert tc.number_of_classes() == 443520 + ``` + +=== "ACE" + + Coming soon! ## The output -Running the above script produces the following output: +=== "Python" -??? info "Output from the Python script" + Running the above script produces the following output: - ``` - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: RUN 0 START (strategy() = hlt) - #0: ToddCoxeter: |A| = 4, |R| = 10, |u| + |v| ∈ [2, 30], ∑(|u| + |v|) = 105 - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.0 START - #0: ToddCoxeter: HLT 0.0.0 | active | killed | defined - #0: ToddCoxeter: nodes | 1 | 0 | 1 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 0 | 4 | 0.0% - #0: ToddCoxeter: time | run 0 = 23µs | all runs = 23µs | elapsed = 78µs - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.0 STOP - #0: ToddCoxeter: HLT 0.0.1 | active | killed | defined - #0: ToddCoxeter: nodes | 5,000,018 | 1,632,158 | 6,632,176 - #0: ToddCoxeter: diff 0.0.0 | +5,000,017 | +1,632,158 | +6,632,175 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 5,679,076 | 14,320,996 | 28.4% - #0: ToddCoxeter: diff 0.0.0 | +5,679,076 | +14,320,992 | +28.4% - #0: ToddCoxeter: phase 0.0 = 418ms | run 0 = 418ms | all runs = 418ms | elapsed = 418ms - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.1 START (lookahead_extent() = partial, lookahead_style() = hlt) - #0: ToddCoxeter: LOOKAHEAD 0.1.0 | active | killed | defined - #0: ToddCoxeter: nodes | 5,000,018 | 1,632,158 | 6,632,176 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 5,679,076 | 14,320,996 | 28.4% - #0: ToddCoxeter: time | run 0 = 418ms | all runs = 418ms | elapsed = 418ms - #0: ToddCoxeter: because a >= n - #0: ToddCoxeter: where: a = number_of_nodes_active() = 5,000,018 - #0: ToddCoxeter: n = lookahead_next() = 5,000,000 - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.1 STOP - #0: ToddCoxeter: LOOKAHEAD 0.1.1 | active | killed | defined - #0: ToddCoxeter: nodes | 2,423,713 | 4,208,463 | 6,632,176 - #0: ToddCoxeter: diff 0.1.0 | -2,576,305 | +2,576,305 | +0 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 7,815,443 | 1,879,409 | 80.6% - #0: ToddCoxeter: diff 0.1.0 | +2,136,367 | -12,441,587 | +52.2% - #0: ToddCoxeter: phase 0.1 = 398ms | run 0 = 816ms | all runs = 816ms | elapsed = 816ms - #0: ToddCoxeter: lookahead_next() is now max(f x a = 4,847,426, m = 10,000) (-152,574) - #0: ToddCoxeter: because f x a < n - #0: ToddCoxeter: where: a = number_of_nodes_active() = 2,423,713 - #0: ToddCoxeter: f = lookahead_growth_factor() = 2 - #0: ToddCoxeter: m = lookahead_min() = 10,000 - #0: ToddCoxeter: n = lookahead_next() = 5,000,000 - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.2 START - #0: ToddCoxeter: HLT 0.2.0 | active | killed | defined - #0: ToddCoxeter: nodes | 2,423,713 | 4,208,463 | 6,632,176 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 7,815,443 | 1,879,409 | 80.6% - #0: ToddCoxeter: time | run 0 = 816ms | all runs = 816ms | elapsed = 816ms - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.2 STOP - #0: ToddCoxeter: HLT 0.2.1 | active | killed | defined - #0: ToddCoxeter: nodes | 4,847,474 | 4,320,458 | 9,167,932 - #0: ToddCoxeter: diff 0.2.0 | +2,423,761 | +111,995 | +2,535,756 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 10,422,837 | 8,967,059 | 53.8% - #0: ToddCoxeter: diff 0.2.0 | +2,607,394 | +7,087,650 | -26.9% - #0: ToddCoxeter: phase 0.2 = 78ms | run 0 = 894ms | all runs = 894ms | elapsed = 894ms - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.3 START (lookahead_extent() = partial, lookahead_style() = hlt) - #0: ToddCoxeter: LOOKAHEAD 0.3.0 | active | killed | defined - #0: ToddCoxeter: nodes | 4,847,474 | 4,320,458 | 9,167,932 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 10,422,837 | 8,967,059 | 53.8% - #0: ToddCoxeter: time | run 0 = 894ms | all runs = 894ms | elapsed = 894ms - #0: ToddCoxeter: because a >= n - #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,847,474 - #0: ToddCoxeter: n = lookahead_next() = 4,847,426 - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.3.1 | active | killed | defined - #1: ToddCoxeter: nodes | 4,720,512 | 4,447,422 | 9,167,932 - #1: ToddCoxeter: diff 0.3.0 | -126,962 | +126,964 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 10,288,113 | 8,593,935 | 54.5% - #1: ToddCoxeter: diff 0.3.0 | -134,724 | -373,124 | +0.7% - #1: ToddCoxeter: phase 0.3 = 105ms | run 0 = 1.000s | all runs = 1.000s | elapsed = 1.000s - #1: ToddCoxeter: lookahead progress | ~17.5% - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.3 STOP - #0: ToddCoxeter: LOOKAHEAD 0.3.2 | active | killed | defined - #0: ToddCoxeter: nodes | 3,512,400 | 5,655,532 | 9,167,932 - #0: ToddCoxeter: diff 0.3.1 | -1,208,112 | +1,208,110 | +0 - #0: ToddCoxeter: diff 0.3.0 | -1,335,074 | +1,335,074 | +0 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 11,491,787 | 2,557,813 | 81.8% - #0: ToddCoxeter: diff 0.3.1 | +1,203,674 | -6,036,122 | +27.3% - #0: ToddCoxeter: diff 0.3.0 | +1,068,950 | -6,409,246 | +28.0% - #0: ToddCoxeter: phase 0.3 = 556ms | run 0 = 1.451s | all runs = 1.451s | elapsed = 1.451s - #0: ToddCoxeter: lookahead_next() is now 4,847,426 (+0) - #0: ToddCoxeter: because: - #0: ToddCoxeter: 1. n <= f x a = 7,024,800 - #0: ToddCoxeter: 2. a <= n - #0: ToddCoxeter: 3. l >= (l + a) / t = 1,211,868 - #0: ToddCoxeter: where: a = number_of_nodes_active() = 3,512,400 - #0: ToddCoxeter: f = lookahead_growth_factor() = 2 - #0: ToddCoxeter: l = nodes killed in lookahead = 1,335,074 - #0: ToddCoxeter: n = lookahead_next() = 4,847,426 - #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.4 START - #0: ToddCoxeter: HLT 0.4.0 | active | killed | defined - #0: ToddCoxeter: nodes | 3,512,400 | 5,655,532 | 9,167,932 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 11,491,787 | 2,557,813 | 81.8% - #0: ToddCoxeter: time | run 0 = 1.451s | all runs = 1.451s | elapsed = 1.451s - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.4 STOP - #0: ToddCoxeter: HLT 0.4.1 | active | killed | defined - #0: ToddCoxeter: nodes | 4,847,449 | 5,703,629 | 10,551,078 - #0: ToddCoxeter: diff 0.4.0 | +1,335,049 | +48,097 | +1,383,146 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 12,934,269 | 6,455,527 | 66.7% - #0: ToddCoxeter: diff 0.4.0 | +1,442,482 | +3,897,714 | -15.1% - #0: ToddCoxeter: phase 0.4 = 62ms | run 0 = 1.513s | all runs = 1.513s | elapsed = 1.514s - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.5 START (lookahead_extent() = partial, lookahead_style() = hlt) - #0: ToddCoxeter: LOOKAHEAD 0.5.0 | active | killed | defined - #0: ToddCoxeter: nodes | 4,847,449 | 5,703,629 | 10,551,078 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 12,934,269 | 6,455,527 | 66.7% - #0: ToddCoxeter: time | run 0 = 1.513s | all runs = 1.513s | elapsed = 1.514s - #0: ToddCoxeter: because a >= n - #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,847,449 - #0: ToddCoxeter: n = lookahead_next() = 4,847,426 - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.5.1 | active | killed | defined - #1: ToddCoxeter: nodes | 4,565,240 | 5,985,863 | 10,551,078 - #1: ToddCoxeter: diff 0.5.0 | -282,209 | +282,234 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 13,023,236 | 5,237,724 | 71.3% - #1: ToddCoxeter: diff 0.5.0 | +88,967 | -1,217,803 | +4.6% - #1: ToddCoxeter: phase 0.5 = 487ms | run 0 = 2.001s | all runs = 2.001s | elapsed = 2.001s - #1: ToddCoxeter: lookahead progress | ~77.2% - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.5 STOP - #0: ToddCoxeter: LOOKAHEAD 0.5.2 | active | killed | defined - #0: ToddCoxeter: nodes | 4,134,106 | 6,416,972 | 10,551,078 - #0: ToddCoxeter: diff 0.5.1 | -431,134 | +431,109 | +0 - #0: ToddCoxeter: diff 0.5.0 | -713,343 | +713,343 | +0 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 13,557,552 | 2,978,872 | 82.0% - #0: ToddCoxeter: diff 0.5.1 | +534,316 | -2,258,852 | +10.7% - #0: ToddCoxeter: diff 0.5.0 | +623,283 | -3,476,655 | +15.3% - #0: ToddCoxeter: phase 0.5 = 642ms | run 0 = 2.156s | all runs = 2.156s | elapsed = 2.156s - #0: ToddCoxeter: lookahead_next() is now n x f = 9,694,852 (+4,847,426) - #0: ToddCoxeter: because: l < (l + a) / t = 1,211,862 - #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,134,106 - #0: ToddCoxeter: f = lookahead_growth_factor() = 2 - #0: ToddCoxeter: l = nodes killed in lookahead = 713,343 - #0: ToddCoxeter: n = lookahead_next() = 4,847,426 - #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.6 START - #0: ToddCoxeter: HLT 0.6.0 | active | killed | defined - #0: ToddCoxeter: nodes | 4,134,106 | 6,416,972 | 10,551,078 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 13,557,552 | 2,978,872 | 82.0% - #0: ToddCoxeter: time | run 0 = 2.156s | all runs = 2.156s | elapsed = 2.156s - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.6 STOP - #0: ToddCoxeter: HLT 0.6.1 | active | killed | defined - #0: ToddCoxeter: nodes | 9,694,873 | 6,657,105 | 16,351,978 - #0: ToddCoxeter: diff 0.6.0 | +5,560,767 | +240,133 | +5,800,900 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 19,575,370 | 19,204,122 | 50.5% - #0: ToddCoxeter: diff 0.6.0 | +6,017,818 | +16,225,250 | -31.5% - #0: ToddCoxeter: phase 0.6 = 425ms | run 0 = 2.582s | all runs = 2.582s | elapsed = 2.582s - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.7 START (lookahead_extent() = partial, lookahead_style() = hlt) - #0: ToddCoxeter: LOOKAHEAD 0.7.0 | active | killed | defined - #0: ToddCoxeter: nodes | 9,694,873 | 6,657,105 | 16,351,978 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 19,575,370 | 19,204,122 | 50.5% - #0: ToddCoxeter: time | run 0 = 2.582s | all runs = 2.582s | elapsed = 2.582s - #0: ToddCoxeter: because a >= n - #0: ToddCoxeter: where: a = number_of_nodes_active() = 9,694,873 - #0: ToddCoxeter: n = lookahead_next() = 9,694,852 - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.7.1 | active | killed | defined - #1: ToddCoxeter: nodes | 9,521,847 | 6,830,131 | 16,351,978 - #1: ToddCoxeter: diff 0.7.0 | -173,026 | +173,026 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 19,432,594 | 18,654,794 | 51.0% - #1: ToddCoxeter: diff 0.7.0 | -142,776 | -549,328 | +0.5% - #1: ToddCoxeter: phase 0.7 = 418ms | run 0 = 3.001s | all runs = 3.001s | elapsed = 3.001s - #1: ToddCoxeter: lookahead progress | ~33.5% - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.7 STOP - #0: ToddCoxeter: LOOKAHEAD 0.7.2 | active | killed | defined - #0: ToddCoxeter: nodes | 6,784,030 | 9,567,948 | 16,351,978 - #0: ToddCoxeter: diff 0.7.1 | -2,737,817 | +2,737,817 | +0 - #0: ToddCoxeter: diff 0.7.0 | -2,910,843 | +2,910,843 | +0 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 22,154,799 | 4,981,321 | 81.6% - #0: ToddCoxeter: diff 0.7.1 | +2,722,205 | -13,673,473 | +30.6% - #0: ToddCoxeter: diff 0.7.0 | +2,579,429 | -14,222,801 | +31.2% - #0: ToddCoxeter: phase 0.7 = 1.109s | run 0 = 3.691s | all runs = 3.691s | elapsed = 3.691s - #0: ToddCoxeter: lookahead_next() is now 9,694,852 (+0) - #0: ToddCoxeter: because: - #0: ToddCoxeter: 1. n <= f x a = 13,568,060 - #0: ToddCoxeter: 2. a <= n - #0: ToddCoxeter: 3. l >= (l + a) / t = 2,423,718 - #0: ToddCoxeter: where: a = number_of_nodes_active() = 6,784,030 - #0: ToddCoxeter: f = lookahead_growth_factor() = 2 - #0: ToddCoxeter: l = nodes killed in lookahead = 2,910,843 - #0: ToddCoxeter: n = lookahead_next() = 9,694,852 - #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.8 START - #0: ToddCoxeter: HLT 0.8.0 | active | killed | defined - #0: ToddCoxeter: nodes | 6,784,030 | 9,567,948 | 16,351,978 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 22,154,799 | 4,981,321 | 81.6% - #0: ToddCoxeter: time | run 0 = 3.691s | all runs = 3.691s | elapsed = 3.691s - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.8 STOP - #0: ToddCoxeter: HLT 0.8.1 | active | killed | defined - #0: ToddCoxeter: nodes | 9,694,854 | 9,675,719 | 19,370,573 - #0: ToddCoxeter: diff 0.8.0 | +2,910,824 | +107,771 | +3,018,595 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 25,297,258 | 13,482,158 | 65.2% - #0: ToddCoxeter: diff 0.8.0 | +3,142,459 | +8,500,837 | -16.4% - #0: ToddCoxeter: phase 0.8 = 113ms | run 0 = 3.805s | all runs = 3.805s | elapsed = 3.805s - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.9 START (lookahead_extent() = partial, lookahead_style() = hlt) - #0: ToddCoxeter: LOOKAHEAD 0.9.0 | active | killed | defined - #0: ToddCoxeter: nodes | 9,694,854 | 9,675,719 | 19,370,573 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 25,297,258 | 13,482,158 | 65.2% - #0: ToddCoxeter: time | run 0 = 3.805s | all runs = 3.805s | elapsed = 3.805s - #0: ToddCoxeter: because a >= n - #0: ToddCoxeter: where: a = number_of_nodes_active() = 9,694,854 - #0: ToddCoxeter: n = lookahead_next() = 9,694,852 - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.9.1 | active | killed | defined - #1: ToddCoxeter: nodes | 9,601,434 | 9,769,139 | 19,370,573 - #1: ToddCoxeter: diff 0.9.0 | -93,420 | +93,420 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 25,215,676 | 13,190,060 | 65.7% - #1: ToddCoxeter: diff 0.9.0 | -81,582 | -292,098 | +0.4% - #1: ToddCoxeter: phase 0.9 = 196ms | run 0 = 4.001s | all runs = 4.001s | elapsed = 4.001s - #1: ToddCoxeter: lookahead progress | ~16.5% - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.9.2 | active | killed | defined - #1: ToddCoxeter: nodes | 8,331,834 | 11,038,768 | 19,370,573 - #1: ToddCoxeter: diff 0.9.1 | -1,269,600 | +1,269,629 | +0 - #1: ToddCoxeter: diff 0.9.0 | -1,363,020 | +1,363,049 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 26,231,811 | 7,095,525 | 78.7% - #1: ToddCoxeter: diff 0.9.1 | +1,016,135 | -6,094,535 | +13.1% - #1: ToddCoxeter: diff 0.9.0 | +934,553 | -6,386,633 | +13.5% - #1: ToddCoxeter: phase 0.9 = 1.197s | run 0 = 5.001s | all runs = 5.001s | elapsed = 5.001s - #1: ToddCoxeter: lookahead progress | ~87.1% - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.9 STOP - #0: ToddCoxeter: LOOKAHEAD 0.9.3 | active | killed | defined - #0: ToddCoxeter: nodes | 8,086,523 | 11,284,050 | 19,370,573 - #0: ToddCoxeter: diff 0.9.2 | -245,311 | +245,282 | +0 - #0: ToddCoxeter: diff 0.9.0 | -1,608,331 | +1,608,331 | +0 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 26,555,088 | 5,791,004 | 82.1% - #0: ToddCoxeter: diff 0.9.2 | +323,277 | -1,304,521 | +3.4% - #0: ToddCoxeter: diff 0.9.0 | +1,257,830 | -7,691,154 | +16.9% - #0: ToddCoxeter: phase 0.9 = 1.320s | run 0 = 5.125s | all runs = 5.125s | elapsed = 5.125s - #0: ToddCoxeter: lookahead_next() is now n x f = 19,389,704 (+9,694,852) - #0: ToddCoxeter: because: l < (l + a) / t = 2,423,713 - #0: ToddCoxeter: where: a = number_of_nodes_active() = 8,086,523 - #0: ToddCoxeter: f = lookahead_growth_factor() = 2 - #0: ToddCoxeter: l = nodes killed in lookahead = 1,608,331 - #0: ToddCoxeter: n = lookahead_next() = 9,694,852 - #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.10 START - #0: ToddCoxeter: HLT 0.10.0 | active | killed | defined - #0: ToddCoxeter: nodes | 8,086,523 | 11,284,050 | 19,370,573 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 26,555,088 | 5,791,004 | 82.1% - #0: ToddCoxeter: time | run 0 = 5.125s | all runs = 5.125s | elapsed = 5.125s - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.10 STOP - #0: ToddCoxeter: HLT 0.10.1 | active | killed | defined - #0: ToddCoxeter: nodes | 19,389,750 | 11,773,835 | 31,163,585 - #0: ToddCoxeter: diff 0.10.0 | +11,303,227 | +489,785 | +11,793,012 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 38,786,740 | 38,772,260 | 50.0% - #0: ToddCoxeter: diff 0.10.0 | +12,231,652 | +32,981,256 | -32.1% - #0: ToddCoxeter: phase 0.10 = 829ms | run 0 = 5.955s | all runs = 5.955s | elapsed = 5.955s - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.11 START (lookahead_extent() = partial, lookahead_style() = hlt) - #0: ToddCoxeter: LOOKAHEAD 0.11.0 | active | killed | defined - #0: ToddCoxeter: nodes | 19,389,750 | 11,773,835 | 31,163,585 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 38,786,740 | 38,772,260 | 50.0% - #0: ToddCoxeter: time | run 0 = 5.955s | all runs = 5.955s | elapsed = 5.955s - #0: ToddCoxeter: because a >= n - #0: ToddCoxeter: where: a = number_of_nodes_active() = 19,389,750 - #0: ToddCoxeter: n = lookahead_next() = 19,389,704 - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.11.1 | active | killed | defined - #1: ToddCoxeter: nodes | 19,361,711 | 11,801,893 | 31,163,585 - #1: ToddCoxeter: diff 0.11.0 | -28,039 | +28,058 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 38,761,553 | 38,685,291 | 50.0% - #1: ToddCoxeter: diff 0.11.0 | -25,187 | -86,969 | +0.0% - #1: ToddCoxeter: phase 0.11 = 46ms | run 0 = 6.002s | all runs = 6.002s | elapsed = 6.002s - #1: ToddCoxeter: lookahead progress | ~4.6% - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.11.2 | active | killed | defined - #1: ToddCoxeter: nodes | 18,900,346 | 12,263,243 | 31,163,585 - #1: ToddCoxeter: diff 0.11.1 | -461,365 | +461,350 | +0 - #1: ToddCoxeter: diff 0.11.0 | -489,404 | +489,408 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 38,376,840 | 37,224,544 | 50.8% - #1: ToddCoxeter: diff 0.11.1 | -384,713 | -1,460,747 | +0.7% - #1: ToddCoxeter: diff 0.11.0 | -409,900 | -1,547,716 | +0.8% - #1: ToddCoxeter: phase 0.11 = 1.047s | run 0 = 7.002s | all runs = 7.002s | elapsed = 7.002s - #1: ToddCoxeter: lookahead progress | ~38.4% - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.11.3 | active | killed | defined - #1: ToddCoxeter: nodes | 14,438,129 | 16,725,554 | 31,163,585 - #1: ToddCoxeter: diff 0.11.2 | -4,462,217 | +4,462,311 | +0 - #1: ToddCoxeter: diff 0.11.0 | -4,951,621 | +4,951,719 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 42,716,669 | 15,035,847 | 74.0% - #1: ToddCoxeter: diff 0.11.2 | +4,339,829 | -22,188,697 | +23.2% - #1: ToddCoxeter: diff 0.11.0 | +3,929,929 | -23,736,413 | +24.0% - #1: ToddCoxeter: phase 0.11 = 2.047s | run 0 = 8.002s | all runs = 8.002s | elapsed = 8.002s - #1: ToddCoxeter: lookahead progress | ~72.2% - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.11 STOP - #0: ToddCoxeter: LOOKAHEAD 0.11.4 | active | killed | defined - #0: ToddCoxeter: nodes | 13,427,510 | 17,736,075 | 31,163,585 - #0: ToddCoxeter: diff 0.11.3 | -1,010,619 | +1,010,521 | +0 - #0: ToddCoxeter: diff 0.11.0 | -5,962,240 | +5,962,240 | +0 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 43,882,513 | 9,827,527 | 81.7% - #0: ToddCoxeter: diff 0.11.3 | +1,165,844 | -5,208,320 | +7.7% - #0: ToddCoxeter: diff 0.11.0 | +5,095,773 | -28,944,733 | +31.7% - #0: ToddCoxeter: phase 0.11 = 2.208s | run 0 = 8.163s | all runs = 8.163s | elapsed = 8.163s - #0: ToddCoxeter: lookahead_next() is now 19,389,704 (+0) - #0: ToddCoxeter: because: - #0: ToddCoxeter: 1. n <= f x a = 26,855,020 - #0: ToddCoxeter: 2. a <= n - #0: ToddCoxeter: 3. l >= (l + a) / t = 4,847,437 - #0: ToddCoxeter: where: a = number_of_nodes_active() = 13,427,510 - #0: ToddCoxeter: f = lookahead_growth_factor() = 2 - #0: ToddCoxeter: l = nodes killed in lookahead = 5,962,240 - #0: ToddCoxeter: n = lookahead_next() = 19,389,704 - #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.12 START - #0: ToddCoxeter: HLT 0.12.0 | active | killed | defined - #0: ToddCoxeter: nodes | 13,427,510 | 17,736,075 | 31,163,585 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 43,882,513 | 9,827,527 | 81.7% - #0: ToddCoxeter: time | run 0 = 8.163s | all runs = 8.163s | elapsed = 8.163s - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.12 STOP - #0: ToddCoxeter: HLT 0.12.1 | active | killed | defined - #0: ToddCoxeter: nodes | 19,389,776 | 17,959,888 | 37,349,664 - #0: ToddCoxeter: diff 0.12.0 | +5,962,266 | +223,813 | +6,186,079 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 50,324,580 | 27,234,524 | 64.9% - #0: ToddCoxeter: diff 0.12.0 | +6,442,067 | +17,406,997 | -16.8% - #0: ToddCoxeter: phase 0.12 = 230ms | run 0 = 8.393s | all runs = 8.393s | elapsed = 8.393s - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.13 START (lookahead_extent() = partial, lookahead_style() = hlt) - #0: ToddCoxeter: LOOKAHEAD 0.13.0 | active | killed | defined - #0: ToddCoxeter: nodes | 19,389,776 | 17,959,888 | 37,349,664 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 50,324,580 | 27,234,524 | 64.9% - #0: ToddCoxeter: time | run 0 = 8.393s | all runs = 8.393s | elapsed = 8.393s - #0: ToddCoxeter: because a >= n - #0: ToddCoxeter: where: a = number_of_nodes_active() = 19,389,776 - #0: ToddCoxeter: n = lookahead_next() = 19,389,704 - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.13.1 | active | killed | defined - #1: ToddCoxeter: nodes | 19,186,302 | 18,163,362 | 37,349,664 - #1: ToddCoxeter: diff 0.13.0 | -203,474 | +203,474 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 50,106,203 | 26,639,005 | 65.3% - #1: ToddCoxeter: diff 0.13.0 | -218,377 | -595,519 | +0.4% - #1: ToddCoxeter: phase 0.13 = 609ms | run 0 = 9.002s | all runs = 9.002s | elapsed = 9.002s - #1: ToddCoxeter: lookahead progress | ~20.7% - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.13.2 | active | killed | defined - #1: ToddCoxeter: nodes | 18,905,330 | 18,444,334 | 37,349,664 - #1: ToddCoxeter: diff 0.13.1 | -280,972 | +280,972 | +0 - #1: ToddCoxeter: diff 0.13.0 | -484,446 | +484,446 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 49,829,308 | 25,792,012 | 65.9% - #1: ToddCoxeter: diff 0.13.1 | -276,895 | -846,993 | +0.6% - #1: ToddCoxeter: diff 0.13.0 | -495,272 | -1,442,512 | +1.0% - #1: ToddCoxeter: phase 0.13 = 1.610s | run 0 = 10.003s | all runs = 10.003s | elapsed = 10.003s - #1: ToddCoxeter: lookahead progress | ~54.1% - #0: ToddCoxeter: large collapse, number of coincidences 100,000 >= 100,000 = large_collapse()! - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.13.3 | active | killed | defined - #1: ToddCoxeter: nodes | 11,154,426 | 26,195,391 | 37,349,664 - #1: ToddCoxeter: diff 0.13.2 | -7,750,904 | +7,751,057 | +0 - #1: ToddCoxeter: diff 0.13.0 | -8,235,350 | +8,235,503 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 0 | 44,617,704 | 0.0% - #1: ToddCoxeter: diff 0.13.2 | -49,829,308 | +18,825,692 | -65.9% - #1: ToddCoxeter: diff 0.13.0 | -50,324,580 | +17,383,180 | -64.9% - #1: ToddCoxeter: phase 0.13 = 2.610s | run 0 = 11.003s | all runs = 11.003s | elapsed = 11.003s - #1: ToddCoxeter: lookahead progress | ~66.6% - ++++++++++++++++++++++++++++++++ - #1: ToddCoxeter: LOOKAHEAD 0.13.4 | active | killed | defined - #1: ToddCoxeter: nodes | 2,148,036 | 35,201,729 | 37,349,664 - #1: ToddCoxeter: diff 0.13.3 | -9,006,390 | +9,006,338 | +0 - #1: ToddCoxeter: diff 0.13.0 | -17,241,740 | +17,241,841 | +0 - #1: ToddCoxeter: | active | missing | % complete - #1: ToddCoxeter: edges | 0 | 8,592,144 | 0.0% - #1: ToddCoxeter: diff 0.13.3 | +0 | -36,025,560 | +0.0% - #1: ToddCoxeter: diff 0.13.0 | -50,324,580 | -18,642,380 | -64.9% - #1: ToddCoxeter: phase 0.13 = 3.610s | run 0 = 12.003s | all runs = 12.003s | elapsed = 12.003s - #1: ToddCoxeter: lookahead progress | ~66.6% - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: LOOKAHEAD 0.13 STOP - #0: ToddCoxeter: LOOKAHEAD 0.13.5 | active | killed | defined - #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 - #0: ToddCoxeter: diff 0.13.4 | -1,704,516 | +1,704,415 | +0 - #0: ToddCoxeter: diff 0.13.0 | -18,946,256 | +18,946,256 | +0 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% - #0: ToddCoxeter: diff 0.13.4 | +1,774,080 | -8,592,144 | +100.0% - #0: ToddCoxeter: diff 0.13.0 | -48,550,500 | -27,234,524 | +35.1% - #0: ToddCoxeter: phase 0.13 = 3.928s | run 0 = 12.321s | all runs = 12.321s | elapsed = 12.321s - #0: ToddCoxeter: lookahead_next() is now max(f x a = 887,040, m = 10,000) (-18,502,664) - #0: ToddCoxeter: because f x a < n - #0: ToddCoxeter: where: a = number_of_nodes_active() = 443,520 - #0: ToddCoxeter: f = lookahead_growth_factor() = 2 - #0: ToddCoxeter: m = lookahead_min() = 10,000 - #0: ToddCoxeter: n = lookahead_next() = 19,389,704 - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.14 START - #0: ToddCoxeter: HLT 0.14.0 | active | killed | defined - #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% - #0: ToddCoxeter: time | run 0 = 12.321s | all runs = 12.321s | elapsed = 12.321s - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.14 STOP - #0: ToddCoxeter: HLT 0.14.1 | active | killed | defined - #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 - #0: ToddCoxeter: diff 0.14.0 | +0 | +0 | +0 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% - #0: ToddCoxeter: diff 0.14.0 | +0 | +0 | +0.0% - #0: ToddCoxeter: phase 0.14 = 108ms | run 0 = 12.430s | all runs = 12.430s | elapsed = 12.430s - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: HLT 0.15.2 | active | killed | defined - #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 - #0: ToddCoxeter: diff 0.15.1 | +0 | +0 | +0 - #0: ToddCoxeter: diff 0.15.0 | +0 | +0 | +0 - #0: ToddCoxeter: | active | missing | % complete - #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% - #0: ToddCoxeter: diff 0.15.1 | +0 | +0 | +0.0% - #0: ToddCoxeter: diff 0.15.0 | +0 | +0 | +0.0% - #0: ToddCoxeter: phase 0.15 = 108ms | run 0 = 12.430s | all runs = 12.430s | elapsed = 12.430s - ++++++++++++++++++++++++++++++++ - #0: ToddCoxeter: RUN 0 STOP (finished) - #0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch - #0: ToddCoxeter: num. phases | 7 | 0 | 8 | 0 - #0: ToddCoxeter: time spent in phases | 10.163s (82%) | - (0%) | 2.267s (18%) | - (0%) - #0: ToddCoxeter: phase 0.15 = 114ms | run 0 = 12.436s | all runs = 12.436s | elapsed = 12.436s - ``` + ??? info "Output from the Python script" + + ``` + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 START (strategy() = hlt) + #0: ToddCoxeter: |A| = 4, |R| = 10, |u| + |v| ∈ [2, 30], ∑(|u| + |v|) = 105 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 START + #0: ToddCoxeter: HLT 0.0.0 | active | killed | defined + #0: ToddCoxeter: nodes | 1 | 0 | 1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 0 | 4 | 0.0% + #0: ToddCoxeter: time | run 0 = 23µs | all runs = 23µs | elapsed = 78µs + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 STOP + #0: ToddCoxeter: HLT 0.0.1 | active | killed | defined + #0: ToddCoxeter: nodes | 5,000,018 | 1,632,158 | 6,632,176 + #0: ToddCoxeter: diff 0.0.0 | +5,000,017 | +1,632,158 | +6,632,175 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 5,679,076 | 14,320,996 | 28.4% + #0: ToddCoxeter: diff 0.0.0 | +5,679,076 | +14,320,992 | +28.4% + #0: ToddCoxeter: phase 0.0 = 418ms | run 0 = 418ms | all runs = 418ms | elapsed = 418ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.1 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.1.0 | active | killed | defined + #0: ToddCoxeter: nodes | 5,000,018 | 1,632,158 | 6,632,176 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 5,679,076 | 14,320,996 | 28.4% + #0: ToddCoxeter: time | run 0 = 418ms | all runs = 418ms | elapsed = 418ms + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 5,000,018 + #0: ToddCoxeter: n = lookahead_next() = 5,000,000 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.1 STOP + #0: ToddCoxeter: LOOKAHEAD 0.1.1 | active | killed | defined + #0: ToddCoxeter: nodes | 2,423,713 | 4,208,463 | 6,632,176 + #0: ToddCoxeter: diff 0.1.0 | -2,576,305 | +2,576,305 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 7,815,443 | 1,879,409 | 80.6% + #0: ToddCoxeter: diff 0.1.0 | +2,136,367 | -12,441,587 | +52.2% + #0: ToddCoxeter: phase 0.1 = 398ms | run 0 = 816ms | all runs = 816ms | elapsed = 816ms + #0: ToddCoxeter: lookahead_next() is now max(f x a = 4,847,426, m = 10,000) (-152,574) + #0: ToddCoxeter: because f x a < n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 2,423,713 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: m = lookahead_min() = 10,000 + #0: ToddCoxeter: n = lookahead_next() = 5,000,000 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.2 START + #0: ToddCoxeter: HLT 0.2.0 | active | killed | defined + #0: ToddCoxeter: nodes | 2,423,713 | 4,208,463 | 6,632,176 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 7,815,443 | 1,879,409 | 80.6% + #0: ToddCoxeter: time | run 0 = 816ms | all runs = 816ms | elapsed = 816ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.2 STOP + #0: ToddCoxeter: HLT 0.2.1 | active | killed | defined + #0: ToddCoxeter: nodes | 4,847,474 | 4,320,458 | 9,167,932 + #0: ToddCoxeter: diff 0.2.0 | +2,423,761 | +111,995 | +2,535,756 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 10,422,837 | 8,967,059 | 53.8% + #0: ToddCoxeter: diff 0.2.0 | +2,607,394 | +7,087,650 | -26.9% + #0: ToddCoxeter: phase 0.2 = 78ms | run 0 = 894ms | all runs = 894ms | elapsed = 894ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.3 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.3.0 | active | killed | defined + #0: ToddCoxeter: nodes | 4,847,474 | 4,320,458 | 9,167,932 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 10,422,837 | 8,967,059 | 53.8% + #0: ToddCoxeter: time | run 0 = 894ms | all runs = 894ms | elapsed = 894ms + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,847,474 + #0: ToddCoxeter: n = lookahead_next() = 4,847,426 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.3.1 | active | killed | defined + #1: ToddCoxeter: nodes | 4,720,512 | 4,447,422 | 9,167,932 + #1: ToddCoxeter: diff 0.3.0 | -126,962 | +126,964 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 10,288,113 | 8,593,935 | 54.5% + #1: ToddCoxeter: diff 0.3.0 | -134,724 | -373,124 | +0.7% + #1: ToddCoxeter: phase 0.3 = 105ms | run 0 = 1.000s | all runs = 1.000s | elapsed = 1.000s + #1: ToddCoxeter: lookahead progress | ~17.5% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.3 STOP + #0: ToddCoxeter: LOOKAHEAD 0.3.2 | active | killed | defined + #0: ToddCoxeter: nodes | 3,512,400 | 5,655,532 | 9,167,932 + #0: ToddCoxeter: diff 0.3.1 | -1,208,112 | +1,208,110 | +0 + #0: ToddCoxeter: diff 0.3.0 | -1,335,074 | +1,335,074 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 11,491,787 | 2,557,813 | 81.8% + #0: ToddCoxeter: diff 0.3.1 | +1,203,674 | -6,036,122 | +27.3% + #0: ToddCoxeter: diff 0.3.0 | +1,068,950 | -6,409,246 | +28.0% + #0: ToddCoxeter: phase 0.3 = 556ms | run 0 = 1.451s | all runs = 1.451s | elapsed = 1.451s + #0: ToddCoxeter: lookahead_next() is now 4,847,426 (+0) + #0: ToddCoxeter: because: + #0: ToddCoxeter: 1. n <= f x a = 7,024,800 + #0: ToddCoxeter: 2. a <= n + #0: ToddCoxeter: 3. l >= (l + a) / t = 1,211,868 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 3,512,400 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 1,335,074 + #0: ToddCoxeter: n = lookahead_next() = 4,847,426 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.4 START + #0: ToddCoxeter: HLT 0.4.0 | active | killed | defined + #0: ToddCoxeter: nodes | 3,512,400 | 5,655,532 | 9,167,932 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 11,491,787 | 2,557,813 | 81.8% + #0: ToddCoxeter: time | run 0 = 1.451s | all runs = 1.451s | elapsed = 1.451s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.4 STOP + #0: ToddCoxeter: HLT 0.4.1 | active | killed | defined + #0: ToddCoxeter: nodes | 4,847,449 | 5,703,629 | 10,551,078 + #0: ToddCoxeter: diff 0.4.0 | +1,335,049 | +48,097 | +1,383,146 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 12,934,269 | 6,455,527 | 66.7% + #0: ToddCoxeter: diff 0.4.0 | +1,442,482 | +3,897,714 | -15.1% + #0: ToddCoxeter: phase 0.4 = 62ms | run 0 = 1.513s | all runs = 1.513s | elapsed = 1.514s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.5 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.5.0 | active | killed | defined + #0: ToddCoxeter: nodes | 4,847,449 | 5,703,629 | 10,551,078 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 12,934,269 | 6,455,527 | 66.7% + #0: ToddCoxeter: time | run 0 = 1.513s | all runs = 1.513s | elapsed = 1.514s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,847,449 + #0: ToddCoxeter: n = lookahead_next() = 4,847,426 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.5.1 | active | killed | defined + #1: ToddCoxeter: nodes | 4,565,240 | 5,985,863 | 10,551,078 + #1: ToddCoxeter: diff 0.5.0 | -282,209 | +282,234 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 13,023,236 | 5,237,724 | 71.3% + #1: ToddCoxeter: diff 0.5.0 | +88,967 | -1,217,803 | +4.6% + #1: ToddCoxeter: phase 0.5 = 487ms | run 0 = 2.001s | all runs = 2.001s | elapsed = 2.001s + #1: ToddCoxeter: lookahead progress | ~77.2% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.5 STOP + #0: ToddCoxeter: LOOKAHEAD 0.5.2 | active | killed | defined + #0: ToddCoxeter: nodes | 4,134,106 | 6,416,972 | 10,551,078 + #0: ToddCoxeter: diff 0.5.1 | -431,134 | +431,109 | +0 + #0: ToddCoxeter: diff 0.5.0 | -713,343 | +713,343 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 13,557,552 | 2,978,872 | 82.0% + #0: ToddCoxeter: diff 0.5.1 | +534,316 | -2,258,852 | +10.7% + #0: ToddCoxeter: diff 0.5.0 | +623,283 | -3,476,655 | +15.3% + #0: ToddCoxeter: phase 0.5 = 642ms | run 0 = 2.156s | all runs = 2.156s | elapsed = 2.156s + #0: ToddCoxeter: lookahead_next() is now n x f = 9,694,852 (+4,847,426) + #0: ToddCoxeter: because: l < (l + a) / t = 1,211,862 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,134,106 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 713,343 + #0: ToddCoxeter: n = lookahead_next() = 4,847,426 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.6 START + #0: ToddCoxeter: HLT 0.6.0 | active | killed | defined + #0: ToddCoxeter: nodes | 4,134,106 | 6,416,972 | 10,551,078 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 13,557,552 | 2,978,872 | 82.0% + #0: ToddCoxeter: time | run 0 = 2.156s | all runs = 2.156s | elapsed = 2.156s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.6 STOP + #0: ToddCoxeter: HLT 0.6.1 | active | killed | defined + #0: ToddCoxeter: nodes | 9,694,873 | 6,657,105 | 16,351,978 + #0: ToddCoxeter: diff 0.6.0 | +5,560,767 | +240,133 | +5,800,900 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 19,575,370 | 19,204,122 | 50.5% + #0: ToddCoxeter: diff 0.6.0 | +6,017,818 | +16,225,250 | -31.5% + #0: ToddCoxeter: phase 0.6 = 425ms | run 0 = 2.582s | all runs = 2.582s | elapsed = 2.582s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.7 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.7.0 | active | killed | defined + #0: ToddCoxeter: nodes | 9,694,873 | 6,657,105 | 16,351,978 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 19,575,370 | 19,204,122 | 50.5% + #0: ToddCoxeter: time | run 0 = 2.582s | all runs = 2.582s | elapsed = 2.582s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 9,694,873 + #0: ToddCoxeter: n = lookahead_next() = 9,694,852 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.7.1 | active | killed | defined + #1: ToddCoxeter: nodes | 9,521,847 | 6,830,131 | 16,351,978 + #1: ToddCoxeter: diff 0.7.0 | -173,026 | +173,026 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 19,432,594 | 18,654,794 | 51.0% + #1: ToddCoxeter: diff 0.7.0 | -142,776 | -549,328 | +0.5% + #1: ToddCoxeter: phase 0.7 = 418ms | run 0 = 3.001s | all runs = 3.001s | elapsed = 3.001s + #1: ToddCoxeter: lookahead progress | ~33.5% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.7 STOP + #0: ToddCoxeter: LOOKAHEAD 0.7.2 | active | killed | defined + #0: ToddCoxeter: nodes | 6,784,030 | 9,567,948 | 16,351,978 + #0: ToddCoxeter: diff 0.7.1 | -2,737,817 | +2,737,817 | +0 + #0: ToddCoxeter: diff 0.7.0 | -2,910,843 | +2,910,843 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 22,154,799 | 4,981,321 | 81.6% + #0: ToddCoxeter: diff 0.7.1 | +2,722,205 | -13,673,473 | +30.6% + #0: ToddCoxeter: diff 0.7.0 | +2,579,429 | -14,222,801 | +31.2% + #0: ToddCoxeter: phase 0.7 = 1.109s | run 0 = 3.691s | all runs = 3.691s | elapsed = 3.691s + #0: ToddCoxeter: lookahead_next() is now 9,694,852 (+0) + #0: ToddCoxeter: because: + #0: ToddCoxeter: 1. n <= f x a = 13,568,060 + #0: ToddCoxeter: 2. a <= n + #0: ToddCoxeter: 3. l >= (l + a) / t = 2,423,718 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 6,784,030 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 2,910,843 + #0: ToddCoxeter: n = lookahead_next() = 9,694,852 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.8 START + #0: ToddCoxeter: HLT 0.8.0 | active | killed | defined + #0: ToddCoxeter: nodes | 6,784,030 | 9,567,948 | 16,351,978 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 22,154,799 | 4,981,321 | 81.6% + #0: ToddCoxeter: time | run 0 = 3.691s | all runs = 3.691s | elapsed = 3.691s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.8 STOP + #0: ToddCoxeter: HLT 0.8.1 | active | killed | defined + #0: ToddCoxeter: nodes | 9,694,854 | 9,675,719 | 19,370,573 + #0: ToddCoxeter: diff 0.8.0 | +2,910,824 | +107,771 | +3,018,595 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 25,297,258 | 13,482,158 | 65.2% + #0: ToddCoxeter: diff 0.8.0 | +3,142,459 | +8,500,837 | -16.4% + #0: ToddCoxeter: phase 0.8 = 113ms | run 0 = 3.805s | all runs = 3.805s | elapsed = 3.805s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.9 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.9.0 | active | killed | defined + #0: ToddCoxeter: nodes | 9,694,854 | 9,675,719 | 19,370,573 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 25,297,258 | 13,482,158 | 65.2% + #0: ToddCoxeter: time | run 0 = 3.805s | all runs = 3.805s | elapsed = 3.805s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 9,694,854 + #0: ToddCoxeter: n = lookahead_next() = 9,694,852 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.9.1 | active | killed | defined + #1: ToddCoxeter: nodes | 9,601,434 | 9,769,139 | 19,370,573 + #1: ToddCoxeter: diff 0.9.0 | -93,420 | +93,420 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 25,215,676 | 13,190,060 | 65.7% + #1: ToddCoxeter: diff 0.9.0 | -81,582 | -292,098 | +0.4% + #1: ToddCoxeter: phase 0.9 = 196ms | run 0 = 4.001s | all runs = 4.001s | elapsed = 4.001s + #1: ToddCoxeter: lookahead progress | ~16.5% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.9.2 | active | killed | defined + #1: ToddCoxeter: nodes | 8,331,834 | 11,038,768 | 19,370,573 + #1: ToddCoxeter: diff 0.9.1 | -1,269,600 | +1,269,629 | +0 + #1: ToddCoxeter: diff 0.9.0 | -1,363,020 | +1,363,049 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 26,231,811 | 7,095,525 | 78.7% + #1: ToddCoxeter: diff 0.9.1 | +1,016,135 | -6,094,535 | +13.1% + #1: ToddCoxeter: diff 0.9.0 | +934,553 | -6,386,633 | +13.5% + #1: ToddCoxeter: phase 0.9 = 1.197s | run 0 = 5.001s | all runs = 5.001s | elapsed = 5.001s + #1: ToddCoxeter: lookahead progress | ~87.1% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.9 STOP + #0: ToddCoxeter: LOOKAHEAD 0.9.3 | active | killed | defined + #0: ToddCoxeter: nodes | 8,086,523 | 11,284,050 | 19,370,573 + #0: ToddCoxeter: diff 0.9.2 | -245,311 | +245,282 | +0 + #0: ToddCoxeter: diff 0.9.0 | -1,608,331 | +1,608,331 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 26,555,088 | 5,791,004 | 82.1% + #0: ToddCoxeter: diff 0.9.2 | +323,277 | -1,304,521 | +3.4% + #0: ToddCoxeter: diff 0.9.0 | +1,257,830 | -7,691,154 | +16.9% + #0: ToddCoxeter: phase 0.9 = 1.320s | run 0 = 5.125s | all runs = 5.125s | elapsed = 5.125s + #0: ToddCoxeter: lookahead_next() is now n x f = 19,389,704 (+9,694,852) + #0: ToddCoxeter: because: l < (l + a) / t = 2,423,713 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 8,086,523 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 1,608,331 + #0: ToddCoxeter: n = lookahead_next() = 9,694,852 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.10 START + #0: ToddCoxeter: HLT 0.10.0 | active | killed | defined + #0: ToddCoxeter: nodes | 8,086,523 | 11,284,050 | 19,370,573 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 26,555,088 | 5,791,004 | 82.1% + #0: ToddCoxeter: time | run 0 = 5.125s | all runs = 5.125s | elapsed = 5.125s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.10 STOP + #0: ToddCoxeter: HLT 0.10.1 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,750 | 11,773,835 | 31,163,585 + #0: ToddCoxeter: diff 0.10.0 | +11,303,227 | +489,785 | +11,793,012 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 38,786,740 | 38,772,260 | 50.0% + #0: ToddCoxeter: diff 0.10.0 | +12,231,652 | +32,981,256 | -32.1% + #0: ToddCoxeter: phase 0.10 = 829ms | run 0 = 5.955s | all runs = 5.955s | elapsed = 5.955s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.11 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.11.0 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,750 | 11,773,835 | 31,163,585 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 38,786,740 | 38,772,260 | 50.0% + #0: ToddCoxeter: time | run 0 = 5.955s | all runs = 5.955s | elapsed = 5.955s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 19,389,750 + #0: ToddCoxeter: n = lookahead_next() = 19,389,704 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.11.1 | active | killed | defined + #1: ToddCoxeter: nodes | 19,361,711 | 11,801,893 | 31,163,585 + #1: ToddCoxeter: diff 0.11.0 | -28,039 | +28,058 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 38,761,553 | 38,685,291 | 50.0% + #1: ToddCoxeter: diff 0.11.0 | -25,187 | -86,969 | +0.0% + #1: ToddCoxeter: phase 0.11 = 46ms | run 0 = 6.002s | all runs = 6.002s | elapsed = 6.002s + #1: ToddCoxeter: lookahead progress | ~4.6% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.11.2 | active | killed | defined + #1: ToddCoxeter: nodes | 18,900,346 | 12,263,243 | 31,163,585 + #1: ToddCoxeter: diff 0.11.1 | -461,365 | +461,350 | +0 + #1: ToddCoxeter: diff 0.11.0 | -489,404 | +489,408 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 38,376,840 | 37,224,544 | 50.8% + #1: ToddCoxeter: diff 0.11.1 | -384,713 | -1,460,747 | +0.7% + #1: ToddCoxeter: diff 0.11.0 | -409,900 | -1,547,716 | +0.8% + #1: ToddCoxeter: phase 0.11 = 1.047s | run 0 = 7.002s | all runs = 7.002s | elapsed = 7.002s + #1: ToddCoxeter: lookahead progress | ~38.4% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.11.3 | active | killed | defined + #1: ToddCoxeter: nodes | 14,438,129 | 16,725,554 | 31,163,585 + #1: ToddCoxeter: diff 0.11.2 | -4,462,217 | +4,462,311 | +0 + #1: ToddCoxeter: diff 0.11.0 | -4,951,621 | +4,951,719 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 42,716,669 | 15,035,847 | 74.0% + #1: ToddCoxeter: diff 0.11.2 | +4,339,829 | -22,188,697 | +23.2% + #1: ToddCoxeter: diff 0.11.0 | +3,929,929 | -23,736,413 | +24.0% + #1: ToddCoxeter: phase 0.11 = 2.047s | run 0 = 8.002s | all runs = 8.002s | elapsed = 8.002s + #1: ToddCoxeter: lookahead progress | ~72.2% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.11 STOP + #0: ToddCoxeter: LOOKAHEAD 0.11.4 | active | killed | defined + #0: ToddCoxeter: nodes | 13,427,510 | 17,736,075 | 31,163,585 + #0: ToddCoxeter: diff 0.11.3 | -1,010,619 | +1,010,521 | +0 + #0: ToddCoxeter: diff 0.11.0 | -5,962,240 | +5,962,240 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 43,882,513 | 9,827,527 | 81.7% + #0: ToddCoxeter: diff 0.11.3 | +1,165,844 | -5,208,320 | +7.7% + #0: ToddCoxeter: diff 0.11.0 | +5,095,773 | -28,944,733 | +31.7% + #0: ToddCoxeter: phase 0.11 = 2.208s | run 0 = 8.163s | all runs = 8.163s | elapsed = 8.163s + #0: ToddCoxeter: lookahead_next() is now 19,389,704 (+0) + #0: ToddCoxeter: because: + #0: ToddCoxeter: 1. n <= f x a = 26,855,020 + #0: ToddCoxeter: 2. a <= n + #0: ToddCoxeter: 3. l >= (l + a) / t = 4,847,437 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 13,427,510 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 5,962,240 + #0: ToddCoxeter: n = lookahead_next() = 19,389,704 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.12 START + #0: ToddCoxeter: HLT 0.12.0 | active | killed | defined + #0: ToddCoxeter: nodes | 13,427,510 | 17,736,075 | 31,163,585 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 43,882,513 | 9,827,527 | 81.7% + #0: ToddCoxeter: time | run 0 = 8.163s | all runs = 8.163s | elapsed = 8.163s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.12 STOP + #0: ToddCoxeter: HLT 0.12.1 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,776 | 17,959,888 | 37,349,664 + #0: ToddCoxeter: diff 0.12.0 | +5,962,266 | +223,813 | +6,186,079 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 50,324,580 | 27,234,524 | 64.9% + #0: ToddCoxeter: diff 0.12.0 | +6,442,067 | +17,406,997 | -16.8% + #0: ToddCoxeter: phase 0.12 = 230ms | run 0 = 8.393s | all runs = 8.393s | elapsed = 8.393s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.13 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.13.0 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,776 | 17,959,888 | 37,349,664 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 50,324,580 | 27,234,524 | 64.9% + #0: ToddCoxeter: time | run 0 = 8.393s | all runs = 8.393s | elapsed = 8.393s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 19,389,776 + #0: ToddCoxeter: n = lookahead_next() = 19,389,704 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.13.1 | active | killed | defined + #1: ToddCoxeter: nodes | 19,186,302 | 18,163,362 | 37,349,664 + #1: ToddCoxeter: diff 0.13.0 | -203,474 | +203,474 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 50,106,203 | 26,639,005 | 65.3% + #1: ToddCoxeter: diff 0.13.0 | -218,377 | -595,519 | +0.4% + #1: ToddCoxeter: phase 0.13 = 609ms | run 0 = 9.002s | all runs = 9.002s | elapsed = 9.002s + #1: ToddCoxeter: lookahead progress | ~20.7% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.13.2 | active | killed | defined + #1: ToddCoxeter: nodes | 18,905,330 | 18,444,334 | 37,349,664 + #1: ToddCoxeter: diff 0.13.1 | -280,972 | +280,972 | +0 + #1: ToddCoxeter: diff 0.13.0 | -484,446 | +484,446 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 49,829,308 | 25,792,012 | 65.9% + #1: ToddCoxeter: diff 0.13.1 | -276,895 | -846,993 | +0.6% + #1: ToddCoxeter: diff 0.13.0 | -495,272 | -1,442,512 | +1.0% + #1: ToddCoxeter: phase 0.13 = 1.610s | run 0 = 10.003s | all runs = 10.003s | elapsed = 10.003s + #1: ToddCoxeter: lookahead progress | ~54.1% + #0: ToddCoxeter: large collapse, number of coincidences 100,000 >= 100,000 = large_collapse()! + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.13.3 | active | killed | defined + #1: ToddCoxeter: nodes | 11,154,426 | 26,195,391 | 37,349,664 + #1: ToddCoxeter: diff 0.13.2 | -7,750,904 | +7,751,057 | +0 + #1: ToddCoxeter: diff 0.13.0 | -8,235,350 | +8,235,503 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 0 | 44,617,704 | 0.0% + #1: ToddCoxeter: diff 0.13.2 | -49,829,308 | +18,825,692 | -65.9% + #1: ToddCoxeter: diff 0.13.0 | -50,324,580 | +17,383,180 | -64.9% + #1: ToddCoxeter: phase 0.13 = 2.610s | run 0 = 11.003s | all runs = 11.003s | elapsed = 11.003s + #1: ToddCoxeter: lookahead progress | ~66.6% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.13.4 | active | killed | defined + #1: ToddCoxeter: nodes | 2,148,036 | 35,201,729 | 37,349,664 + #1: ToddCoxeter: diff 0.13.3 | -9,006,390 | +9,006,338 | +0 + #1: ToddCoxeter: diff 0.13.0 | -17,241,740 | +17,241,841 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 0 | 8,592,144 | 0.0% + #1: ToddCoxeter: diff 0.13.3 | +0 | -36,025,560 | +0.0% + #1: ToddCoxeter: diff 0.13.0 | -50,324,580 | -18,642,380 | -64.9% + #1: ToddCoxeter: phase 0.13 = 3.610s | run 0 = 12.003s | all runs = 12.003s | elapsed = 12.003s + #1: ToddCoxeter: lookahead progress | ~66.6% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.13 STOP + #0: ToddCoxeter: LOOKAHEAD 0.13.5 | active | killed | defined + #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 + #0: ToddCoxeter: diff 0.13.4 | -1,704,516 | +1,704,415 | +0 + #0: ToddCoxeter: diff 0.13.0 | -18,946,256 | +18,946,256 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% + #0: ToddCoxeter: diff 0.13.4 | +1,774,080 | -8,592,144 | +100.0% + #0: ToddCoxeter: diff 0.13.0 | -48,550,500 | -27,234,524 | +35.1% + #0: ToddCoxeter: phase 0.13 = 3.928s | run 0 = 12.321s | all runs = 12.321s | elapsed = 12.321s + #0: ToddCoxeter: lookahead_next() is now max(f x a = 887,040, m = 10,000) (-18,502,664) + #0: ToddCoxeter: because f x a < n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 443,520 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: m = lookahead_min() = 10,000 + #0: ToddCoxeter: n = lookahead_next() = 19,389,704 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.14 START + #0: ToddCoxeter: HLT 0.14.0 | active | killed | defined + #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% + #0: ToddCoxeter: time | run 0 = 12.321s | all runs = 12.321s | elapsed = 12.321s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.14 STOP + #0: ToddCoxeter: HLT 0.14.1 | active | killed | defined + #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 + #0: ToddCoxeter: diff 0.14.0 | +0 | +0 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% + #0: ToddCoxeter: diff 0.14.0 | +0 | +0 | +0.0% + #0: ToddCoxeter: phase 0.14 = 108ms | run 0 = 12.430s | all runs = 12.430s | elapsed = 12.430s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.15.2 | active | killed | defined + #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 + #0: ToddCoxeter: diff 0.15.1 | +0 | +0 | +0 + #0: ToddCoxeter: diff 0.15.0 | +0 | +0 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% + #0: ToddCoxeter: diff 0.15.1 | +0 | +0 | +0.0% + #0: ToddCoxeter: diff 0.15.0 | +0 | +0 | +0.0% + #0: ToddCoxeter: phase 0.15 = 108ms | run 0 = 12.430s | all runs = 12.430s | elapsed = 12.430s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 STOP (finished) + #0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch + #0: ToddCoxeter: num. phases | 7 | 0 | 8 | 0 + #0: ToddCoxeter: time spent in phases | 10.163s (82%) | - (0%) | 2.267s (18%) | - (0%) + #0: ToddCoxeter: phase 0.15 = 114ms | run 0 = 12.436s | all runs = 12.436s | elapsed = 12.436s + ``` + +=== "ACE" + + Coming soon! :simple-ticktick: The computed size of the group matches the size of the group provided on [the ATLAS][atlas]: $443,520$. [atlas]: https://brauer.maths.qmul.ac.uk/Atlas/v3/spor/ -[libsemigroups_pybind11]: https://libsemigroups.github.io/libsemigroups_pybind11/index.html +[libsemigroups_pybind11]: + https://libsemigroups.github.io/libsemigroups_pybind11/index.html diff --git a/mkdocs.yml b/mkdocs.yml index fd19a6f..18b827c 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -76,6 +76,7 @@ theme: - content.code.copy - content.code.select - content.footnote.tooltips + - content.tabs.link plugins: # - optimize From ae5e6312a16709cae0f7037f52ae71a651113446 Mon Sep 17 00:00:00 2001 From: Joseph Edwards Date: Tue, 2 Jun 2026 13:26:28 +0100 Subject: [PATCH 7/7] Add ACE tabs in stubs --- docs/examples/atlas/leech-lattice/hs.md | 20 ++++++++++++++++---- docs/examples/atlas/leech-lattice/j2.md | 20 ++++++++++++++++---- docs/examples/atlas/misc/t.md | 16 ++++++++++++++-- docs/examples/atlas/pariahs/j1.md | 20 ++++++++++++++++---- docs/examples/atlas/pariahs/j3.md | 20 ++++++++++++++++---- 5 files changed, 78 insertions(+), 18 deletions(-) diff --git a/docs/examples/atlas/leech-lattice/hs.md b/docs/examples/atlas/leech-lattice/hs.md index 0f288c3..01d3061 100644 --- a/docs/examples/atlas/leech-lattice/hs.md +++ b/docs/examples/atlas/leech-lattice/hs.md @@ -4,13 +4,25 @@ > Presentation: TODO -On this page, we verify that the above claimed presentation of the Higman-Sims -group HS defines a group of order $44,352,000$. +On this page, we verify that the above claimed presentation of the Higman-Sims group HS +defines a group of order $44,352,000$. ## The code -Coming soon! +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! ## The output -Coming soon! +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! diff --git a/docs/examples/atlas/leech-lattice/j2.md b/docs/examples/atlas/leech-lattice/j2.md index 4bf4d81..ad93c5e 100644 --- a/docs/examples/atlas/leech-lattice/j2.md +++ b/docs/examples/atlas/leech-lattice/j2.md @@ -4,13 +4,25 @@ > Presentation: TODO -On this page, we verify that the above claimed presentation of the Janko group -J~2~ defines a group of order $604,800$. +On this page, we verify that the above claimed presentation of the Janko group J~2~ +defines a group of order $604,800$. ## The code -Coming soon! +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! ## The output -Coming soon! +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! diff --git a/docs/examples/atlas/misc/t.md b/docs/examples/atlas/misc/t.md index 92815d9..512ded2 100644 --- a/docs/examples/atlas/misc/t.md +++ b/docs/examples/atlas/misc/t.md @@ -9,8 +9,20 @@ defines a group of order $17,971,200$. ## The code -Coming soon! +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! ## The output -Coming soon! +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! diff --git a/docs/examples/atlas/pariahs/j1.md b/docs/examples/atlas/pariahs/j1.md index 5f866fd..ef2c3d5 100644 --- a/docs/examples/atlas/pariahs/j1.md +++ b/docs/examples/atlas/pariahs/j1.md @@ -4,13 +4,25 @@ > Presentation: TODO -On this page, we verify that the above claimed presentation of the Janko group -J~1~ defines a group of order $175,560$. +On this page, we verify that the above claimed presentation of the Janko group J~1~ +defines a group of order $175,560$. ## The code -Coming soon! +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! ## The output -Coming soon! +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! diff --git a/docs/examples/atlas/pariahs/j3.md b/docs/examples/atlas/pariahs/j3.md index 11a96a0..4962867 100644 --- a/docs/examples/atlas/pariahs/j3.md +++ b/docs/examples/atlas/pariahs/j3.md @@ -4,13 +4,25 @@ > Presentation: TODO -On this page, we verify that the above claimed presentation of the Janko group -J~3~ defines a group of order $50,232,960$. +On this page, we verify that the above claimed presentation of the Janko group J~3~ +defines a group of order $50,232,960$. ## The code -Coming soon! +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! ## The output -Coming soon! +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon!