Search space for (EqX ∧ EqY) → EqZ

Stream: Equational

[Vlad Tsyrklevich]

I had the thought that if we were to redo this project with what we know now, we would know that the search space is much smaller than it might have initially seemed--instead of 4694^2≈22m combinations, the actual search space is closer to ~1420^2≈2m after collapsing equivalence classes and another halving after considering duals. I began to wonder if there would be a similarly large reduction in searching for the implications of the conjunction of any two of the original 4,694 equations to the same set based on knowledge of the EqX → EqZ case and decided to calculate it on a whim.

Naively, the space is 4694^3≈103b but after collapsing equivalence classes it is 1420^3≈2.8b. We can do better by a simple algorithm: Fix X<Y. If EqX is a descendant of EqY or vice versa, the problem is already solved (it's simply the implications of the ancestor.) Otherwise, we find EqX and EqY's lowest common ancestors, compute their closures, and subtract the closures of the LCAs from that of EqX and EqY. We must search all of those implications. I conjectured that the reduction would be rather large, but it only reduced the space to ~785m, with a further 2x reduction by duals [unless I'm mistaken, is it sure that if (EqX ∧ EqY) → EqZ that (dual(EqX) ∧ dual(EqY)) → dual(EqZ)?]

This is perhaps a poor method of estimating the problem size, since in the conjunction case it may be much harder to apply the same tools to refute implications and there won't be any equivalence classes to reduce the search space. I just thought to share in case anyone found it as interesting as I did to consider.

[Zoltan A. Kocsis (Z.A.K.)]

As an initial test, one could gather the existing finite counterexample magmas and see how many such implications they refute.

[Terence Tao]

Thanks for this. So naively it could be two or three orders of magnitude more complex to get the triple intersections. Once one fixes X, and just looks at Y->Z relative to X, one is back to an implication graph problem and so in particular we get to use transitivity again. I imagine the finite magmas and also the newer linear magmas will also eliminate a lot of cases. It's also possible that by performing transitivity on the graph on 4694^2 classes (one for each pair X,Y) rather than 4694 classes, one can get a lot more mileage out of transitivity. This begins to get quite CPU-intensive though.

I feel like we need more input from the universal algebraists as to what kind of data sets might actually be useful for their work beyond this proof of concept.

[Vlad Tsyrklevich]

I had not considered that by fixing X, you get back to the same problem as what we have now. That does actually change how difficult it seems. Now you get the same tools and speed-ups as we have now, but just on ~1420 problems, each individually smaller on average, 785m/~1420≈550k instead of ~2m. I imagine the average case may collapse into a few huge equivalence classes, and that implications becomes easier while refutation becomes harder.

[Will Sawin]

Transitivity for the X-fixed problem can be stated as (X and Y) implies Z together with (X and Z) implies W gives (X and Y) implies W. Stated this way it's clear you can chain together in multiple ways, like if Y and W implies something you can use that as well. So there are advantages to considering the different problems together.

[Bruno Le Floch]

(Reviving an ancient topic because today I could run some long code while dealing with non-work stuff.)

If we restrict to laws of order up to 2 and consider all conjunctions X1∧X2∧...∧Xk, using an ATP (prover9) I get that there are at most 28 distinct equivalence classes other than those equivalent to an order ≤4 law, with the following representatives and some disorganised comments.

• (3, 10) unclear x=x◇x and x=x◇(y◇x)
• (3, 14) ⇔ 4961 (law of order five) characterizes Mendelsohn quasigroups;
• (3, 14, 16) ⇔ (3, 14, 16, 26, 43) ⇔ 4964 (law of order five) characterizes squags (idempotent totally-symmetric quasigroups);
• (3, 16) unclear, constrains all left multiplications independently
• (3, 43) idempotence and commutativity
• (8, 23) x=x◇(x◇x)=(x◇x)◇x single-variable equations
• (8, 26) unclear x=x◇(x◇x) and x=(x◇y)◇y
• (8, 26, 31) ⇔ (11, 26, 31, 40) ⇔ unit-unipotence (all squares equal to a unique both-sided unit), and right-multiplications square to the identity
• (8, 31) only constrains multiplications by squares
• (8, 40) ⇔ (11, 40) right-unit unipotent law
• (8, 43) ⇔ (8, 23, 43) ⇔ commutative and x=x◇(x◇x)
• (9, 26) unclear x=x◇(x◇y) and x=(x◇y)◇y
• (10, 25) ⇔ (3, 10, 25) unclear x=x◇x=x◇(y◇x)=(x◇y)◇x
• (10, 40) ⇔ (10, 11, 40) unclear, implies "right-unit left-zero unipotence"
• (11, 14, 16) ⇔ (11, 14, 16, 26, 31, 40, 43) ⇔ 63702 (of order six) characterizing sloops
• (11, 26) unclear, constrains all right-multiplications independently
• (11, 31) ⇔ (11, 31, 40) ⇔ unit-unipotence
• (11, 43) ⇔ (11, 31, 40, 43) ⇔ commutativity and unit-unipotence
• (40, 43) ⇔ commutativity and unipotence (all squares equal)
• and their duals: (3, 25), (3, 26), (16, 23), (11, 16, 23), (11, 23), (23, 40), (16, 28), (25, 40), (16, 31)

Here are some numbers to estimate what may happen at higher orders. There are respectively 5, 23, 146, 1415 equivalence classes of laws of order ≤1, ≤2, ≤3, ≤4. Naively, that means 10, 253, 10585, 1000405 pairs {X,Y} with X,Y representatives of equivalence classes with such orders. Excluding the cases where X⇒Y or X⇐Y reduces these numbers to 1, 162, 9472, and 971983 I think. For most of these pairs, X∧Y is equivalent to a single one of our laws, often 2, 4, 5, or other pretty strong laws. Specifically, at orders ≤1, ≤2, ≤3, there are 1, 132, 6350 pairs equivalent to a single law. That leaves 0, 30, 3122 interesting pairs.

[Bruno Le Floch]

(Edited to reorganize the data.) There are 59 equivalence classes of conjunctions of laws of order up to 2, and a quick ATP run provides the whole implication graph between these. First, a list of representatives of these classes, with an equivalent higher-order law when known.

Representatives of equivalence classes of conjunctions

1
2
3
4
5
8
9
10
11
13
14
16
23
24
25
26
28
31
38
39
40
41
43
3 ∧ 10
3 ∧ 14 (⇔ 4961)
3 ∧ 16
3 ∧ 25
3 ∧ 26
3 ∧ 43
8 ∧ 23
8 ∧ 26
8 ∧ 31
8 ∧ 40
8 ∧ 43
9 ∧ 10 (⇔ 428)
9 ∧ 26
10 ∧ 11 (⇔ 434)
10 ∧ 25
10 ∧ 40
11 ∧ 14 (⇔ 887)
11 ∧ 16 (⇔ 508)
11 ∧ 23
11 ∧ 26
11 ∧ 31
11 ∧ 43
14 ∧ 16 (⇔ 492)
16 ∧ 23
16 ∧ 28
16 ∧ 31
23 ∧ 40
25 ∧ 28 (⇔ 3108)
25 ∧ 31 (⇔ 3145)
25 ∧ 40
26 ∧ 31 (⇔ 1726)
40 ∧ 43
3 ∧ 14 ∧ 16 (⇔ 4964)
8 ∧ 26 ∧ 31 (⇔ 271251)
11 ∧ 14 ∧ 16 (⇔ 63702)
11 ∧ 16 ∧ 23 (⇔ 68410)

Then the minimal implications that generate all of the implications by transitivity. We include here obvious implications such as 3 ∧ 10 ⇒ 10.

Minimal implications that generate the whole graph

2 ⇒ 4
2 ⇒ 5
2 ⇒ 41
2 ⇒ 10 ∧ 40
2 ⇒ 25 ∧ 40
2 ⇒ 3 ∧ 14 ∧ 16
2 ⇒ 11 ∧ 14 ∧ 16
3 ⇒ 8 ∧ 23
4 ⇒ 24
4 ⇒ 9 ∧ 10
4 ⇒ 9 ∧ 26
4 ⇒ 10 ∧ 11
4 ⇒ 10 ∧ 25
4 ⇒ 11 ∧ 26
5 ⇒ 13
5 ⇒ 25 ∧ 28
5 ⇒ 25 ∧ 31
5 ⇒ 10 ∧ 25
5 ⇒ 16 ∧ 28
5 ⇒ 16 ∧ 31
8 ⇒ 1
9 ⇒ 3
10 ⇒ 8
11 ⇒ 8
13 ⇒ 10
13 ⇒ 16
13 ⇒ 39
14 ⇒ 8 ∧ 23
16 ⇒ 8
23 ⇒ 1
24 ⇒ 25
24 ⇒ 26
24 ⇒ 38
25 ⇒ 23
26 ⇒ 23
28 ⇒ 3
31 ⇒ 23
38 ⇒ 1
39 ⇒ 1
40 ⇒ 1
41 ⇒ 38
41 ⇒ 39
41 ⇒ 40 ∧ 43
43 ⇒ 1
3 ∧ 10 ⇒ 3
3 ∧ 10 ⇒ 10
3 ∧ 14 ⇒ 3
3 ∧ 14 ⇒ 14
3 ∧ 16 ⇒ 3
3 ∧ 16 ⇒ 16 ∧ 23
3 ∧ 25 ⇒ 3
3 ∧ 25 ⇒ 25
3 ∧ 26 ⇒ 3
3 ∧ 26 ⇒ 8 ∧ 26
3 ∧ 43 ⇒ 3
3 ∧ 43 ⇒ 8 ∧ 43
8 ∧ 23 ⇒ 8
8 ∧ 23 ⇒ 23
8 ∧ 26 ⇒ 26
8 ∧ 26 ⇒ 8 ∧ 23
8 ∧ 31 ⇒ 31
8 ∧ 31 ⇒ 8 ∧ 23
8 ∧ 40 ⇒ 11
8 ∧ 40 ⇒ 40
8 ∧ 43 ⇒ 43
8 ∧ 43 ⇒ 8 ∧ 23
9 ∧ 10 ⇒ 9
9 ∧ 10 ⇒ 3 ∧ 10
9 ∧ 26 ⇒ 9
9 ∧ 26 ⇒ 3 ∧ 26
10 ∧ 11 ⇒ 10
10 ∧ 11 ⇒ 11
10 ∧ 25 ⇒ 3 ∧ 10
10 ∧ 25 ⇒ 3 ∧ 25
10 ∧ 40 ⇒ 8 ∧ 40
10 ∧ 40 ⇒ 10 ∧ 11
11 ∧ 14 ⇒ 14
11 ∧ 14 ⇒ 11 ∧ 31
11 ∧ 16 ⇒ 16
11 ∧ 16 ⇒ 8 ∧ 40
11 ∧ 23 ⇒ 11
11 ∧ 23 ⇒ 8 ∧ 23
11 ∧ 26 ⇒ 8 ∧ 26
11 ∧ 26 ⇒ 11 ∧ 23
11 ∧ 31 ⇒ 8 ∧ 31
11 ∧ 31 ⇒ 8 ∧ 40
11 ∧ 31 ⇒ 11 ∧ 23
11 ∧ 31 ⇒ 23 ∧ 40
11 ∧ 43 ⇒ 8 ∧ 43
11 ∧ 43 ⇒ 11 ∧ 31
11 ∧ 43 ⇒ 40 ∧ 43
14 ∧ 16 ⇒ 14
14 ∧ 16 ⇒ 8 ∧ 26
14 ∧ 16 ⇒ 8 ∧ 43
14 ∧ 16 ⇒ 16 ∧ 23
16 ∧ 23 ⇒ 16
16 ∧ 23 ⇒ 8 ∧ 23
16 ∧ 28 ⇒ 28
16 ∧ 28 ⇒ 3 ∧ 16
16 ∧ 31 ⇒ 8 ∧ 31
16 ∧ 31 ⇒ 16 ∧ 23
23 ∧ 40 ⇒ 31
23 ∧ 40 ⇒ 40
25 ∧ 28 ⇒ 28
25 ∧ 28 ⇒ 3 ∧ 25
25 ∧ 31 ⇒ 25
25 ∧ 31 ⇒ 31
25 ∧ 40 ⇒ 23 ∧ 40
25 ∧ 40 ⇒ 25 ∧ 31
26 ∧ 31 ⇒ 26
26 ∧ 31 ⇒ 23 ∧ 40
40 ∧ 43 ⇒ 40
40 ∧ 43 ⇒ 43
3 ∧ 14 ∧ 16 ⇒ 3 ∧ 14
3 ∧ 14 ∧ 16 ⇒ 3 ∧ 16
3 ∧ 14 ∧ 16 ⇒ 3 ∧ 26
3 ∧ 14 ∧ 16 ⇒ 3 ∧ 43
3 ∧ 14 ∧ 16 ⇒ 14 ∧ 16
8 ∧ 26 ∧ 31 ⇒ 11 ∧ 26
8 ∧ 26 ∧ 31 ⇒ 11 ∧ 31
8 ∧ 26 ∧ 31 ⇒ 26 ∧ 31
11 ∧ 14 ∧ 16 ⇒ 11 ∧ 14
11 ∧ 14 ∧ 16 ⇒ 11 ∧ 43
11 ∧ 14 ∧ 16 ⇒ 14 ∧ 16
11 ∧ 14 ∧ 16 ⇒ 8 ∧ 26 ∧ 31
11 ∧ 14 ∧ 16 ⇒ 11 ∧ 16 ∧ 23
11 ∧ 16 ∧ 23 ⇒ 11 ∧ 16
11 ∧ 16 ∧ 23 ⇒ 11 ∧ 31
11 ∧ 16 ∧ 23 ⇒ 16 ∧ 31

In principle, this is enough data to determine all conjunctions: indeed, by my claim that the list of 59 is complete, the conjunction of two representatives R1 and R2 must be some other representative, and it must be the meet of R1 and R2 in the lattice generated by the above implications.

To arrive at my list I first determined which pairs of laws reduce to a law in the list. Besides X∧Y⇔X whenever X⇒Y, the list of such pairs is as follows.

Equivalence of two-way conjunctions and low-order laws

3 ∧ 11 ⇔ 4
3 ∧ 13 ⇔ 5
3 ∧ 24 ⇔ 4
3 ∧ 31 ⇔ 5
3 ∧ 38 ⇔ 4
3 ∧ 39 ⇔ 5
3 ∧ 40 ⇔ 2
3 ∧ 41 ⇔ 2
4 ∧ 5 ⇔ 2
4 ∧ 13 ⇔ 2
4 ∧ 14 ⇔ 2
4 ∧ 16 ⇔ 2
4 ∧ 28 ⇔ 2
4 ∧ 31 ⇔ 2
4 ∧ 39 ⇔ 2
4 ∧ 40 ⇔ 2
4 ∧ 41 ⇔ 2
4 ∧ 43 ⇔ 2
5 ∧ 9 ⇔ 2
5 ∧ 11 ⇔ 2
5 ∧ 14 ⇔ 2
5 ∧ 24 ⇔ 2
5 ∧ 26 ⇔ 2
5 ∧ 38 ⇔ 2
5 ∧ 40 ⇔ 2
5 ∧ 41 ⇔ 2
5 ∧ 43 ⇔ 2
8 ∧ 24 ⇔ 4
8 ∧ 38 ⇔ 4
8 ∧ 39 ⇔ 13
8 ∧ 41 ⇔ 2
9 ∧ 11 ⇔ 4
9 ∧ 13 ⇔ 2
9 ∧ 14 ⇔ 2
9 ∧ 16 ⇔ 2
9 ∧ 24 ⇔ 4
9 ∧ 25 ⇔ 4
9 ∧ 28 ⇔ 2
9 ∧ 31 ⇔ 2
9 ∧ 38 ⇔ 4
9 ∧ 39 ⇔ 2
9 ∧ 40 ⇔ 2
9 ∧ 41 ⇔ 2
9 ∧ 43 ⇔ 2
10 ∧ 14 ⇔ 2
10 ∧ 16 ⇔ 13
10 ∧ 24 ⇔ 4
10 ∧ 26 ⇔ 4
10 ∧ 28 ⇔ 5
10 ∧ 31 ⇔ 5
10 ∧ 38 ⇔ 4
10 ∧ 39 ⇔ 13
10 ∧ 41 ⇔ 2
10 ∧ 43 ⇔ 2
11 ∧ 13 ⇔ 2
11 ∧ 24 ⇔ 4
11 ∧ 25 ⇔ 4
11 ∧ 28 ⇔ 2
11 ∧ 38 ⇔ 4
11 ∧ 39 ⇔ 2
11 ∧ 41 ⇔ 2
13 ∧ 14 ⇔ 2
13 ∧ 23 ⇔ 5
13 ∧ 24 ⇔ 2
13 ∧ 25 ⇔ 5
13 ∧ 26 ⇔ 2
13 ∧ 28 ⇔ 5
13 ∧ 31 ⇔ 5
13 ∧ 38 ⇔ 2
13 ∧ 40 ⇔ 2
13 ∧ 41 ⇔ 2
13 ∧ 43 ⇔ 2
14 ∧ 24 ⇔ 2
14 ∧ 25 ⇔ 2
14 ∧ 28 ⇔ 2
14 ∧ 38 ⇔ 2
14 ∧ 39 ⇔ 2
14 ∧ 41 ⇔ 2
16 ∧ 24 ⇔ 2
16 ∧ 25 ⇔ 5
16 ∧ 38 ⇔ 2
16 ∧ 39 ⇔ 13
16 ∧ 41 ⇔ 2
23 ∧ 38 ⇔ 24
23 ∧ 39 ⇔ 5
23 ∧ 41 ⇔ 2
24 ∧ 28 ⇔ 2
24 ∧ 31 ⇔ 2
24 ∧ 39 ⇔ 2
24 ∧ 40 ⇔ 2
24 ∧ 41 ⇔ 2
24 ∧ 43 ⇔ 2
25 ∧ 26 ⇔ 24
25 ∧ 38 ⇔ 24
25 ∧ 39 ⇔ 5
25 ∧ 41 ⇔ 2
25 ∧ 43 ⇔ 2
26 ∧ 28 ⇔ 2
26 ∧ 38 ⇔ 24
26 ∧ 39 ⇔ 2
26 ∧ 41 ⇔ 2
28 ∧ 31 ⇔ 5
28 ∧ 38 ⇔ 2
28 ∧ 39 ⇔ 5
28 ∧ 40 ⇔ 2
28 ∧ 41 ⇔ 2
28 ∧ 43 ⇔ 2
31 ∧ 38 ⇔ 2
31 ∧ 39 ⇔ 5
31 ∧ 41 ⇔ 2
38 ∧ 39 ⇔ 41
38 ∧ 40 ⇔ 41
38 ∧ 43 ⇔ 41
39 ∧ 40 ⇔ 41
39 ∧ 43 ⇔ 41

At this point, any conjunction of low-order laws can be reduced to one where none of these pairs appear. One only needs to consider cliques in the complementary graph (whose edges are pairs that do not simplify in that way). Here are the equivalences between such cliques and the representatives mentioned above.

Equivalences for more complicated conjunctions

14 ∧ 26 ⇔ 14 ∧ 16
14 ∧ 43 ⇔ 14 ∧ 16
14 ∧ 31 ⇔ 11 ∧ 14
14 ∧ 40 ⇔ 11 ∧ 14
16 ∧ 26 ⇔ 14 ∧ 16
16 ∧ 43 ⇔ 14 ∧ 16
16 ∧ 40 ⇔ 11 ∧ 16
26 ∧ 43 ⇔ 14 ∧ 16
26 ∧ 40 ⇔ 26 ∧ 31
10 ∧ 25 ∧ 40 ⇔ 2
10 ∧ 23 ∧ 40 ⇔ 2
10 ∧ 11 ∧ 23 ⇔ 4
14 ∧ 16 ∧ 26 ⇔ 14 ∧ 16
14 ∧ 16 ∧ 43 ⇔ 14 ∧ 16
14 ∧ 26 ∧ 43 ⇔ 14 ∧ 16
14 ∧ 31 ∧ 40 ⇔ 11 ∧ 14
11 ∧ 14 ∧ 31 ⇔ 11 ∧ 14
11 ∧ 14 ∧ 40 ⇔ 11 ∧ 14
16 ∧ 26 ∧ 43 ⇔ 14 ∧ 16
16 ∧ 23 ∧ 43 ⇔ 14 ∧ 16
11 ∧ 16 ∧ 40 ⇔ 11 ∧ 16
8 ∧ 25 ∧ 31 ⇔ 5
8 ∧ 25 ∧ 40 ⇔ 2
8 ∧ 26 ∧ 43 ⇔ 14 ∧ 16
26 ∧ 31 ∧ 40 ⇔ 26 ∧ 31
10 ∧ 11 ∧ 23 ∧ 40 ⇔ 2
14 ∧ 16 ∧ 26 ∧ 43 ⇔ 14 ∧ 16
11 ∧ 14 ∧ 31 ∧ 40 ⇔ 11 ∧ 14
8 ∧ 25 ∧ 31 ∧ 40 ⇔ 2
10 ∧ 23 ⇔ 3 ∧ 10
8 ∧ 25 ⇔ 3 ∧ 25
23 ∧ 43 ⇔ 8 ∧ 43
31 ∧ 43 ⇔ 11 ∧ 43
31 ∧ 40 ⇔ 23 ∧ 40
11 ∧ 40 ⇔ 8 ∧ 40
3 ∧ 10 ∧ 25 ⇔ 10 ∧ 25
3 ∧ 14 ∧ 26 ⇔ 3 ∧ 14 ∧ 16
3 ∧ 14 ∧ 43 ⇔ 3 ∧ 14 ∧ 16
3 ∧ 16 ∧ 26 ⇔ 3 ∧ 14 ∧ 16
3 ∧ 16 ∧ 43 ⇔ 3 ∧ 14 ∧ 16
3 ∧ 26 ∧ 43 ⇔ 3 ∧ 14 ∧ 16
10 ∧ 11 ∧ 40 ⇔ 10 ∧ 40
14 ∧ 16 ∧ 31 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 16 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 26 ∧ 31 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 26 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 26 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
16 ∧ 26 ∧ 31 ⇔ 11 ∧ 14 ∧ 16
16 ∧ 26 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 26 ⇔ 11 ∧ 14 ∧ 16
16 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
16 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
16 ∧ 23 ∧ 40 ⇔ 11 ∧ 16 ∧ 23
16 ∧ 31 ∧ 40 ⇔ 11 ∧ 16 ∧ 23
11 ∧ 16 ∧ 31 ⇔ 11 ∧ 16 ∧ 23
25 ∧ 31 ∧ 40 ⇔ 25 ∧ 40
26 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
26 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 26 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
8 ∧ 26 ∧ 40 ⇔ 8 ∧ 26 ∧ 31
11 ∧ 26 ∧ 31 ⇔ 8 ∧ 26 ∧ 31
11 ∧ 26 ∧ 40 ⇔ 8 ∧ 26 ∧ 31
8 ∧ 23 ∧ 43 ⇔ 8 ∧ 43
8 ∧ 31 ∧ 43 ⇔ 11 ∧ 43
8 ∧ 40 ∧ 43 ⇔ 11 ∧ 43
23 ∧ 40 ∧ 43 ⇔ 11 ∧ 43
11 ∧ 23 ∧ 43 ⇔ 11 ∧ 43
31 ∧ 40 ∧ 43 ⇔ 11 ∧ 43
11 ∧ 31 ∧ 43 ⇔ 11 ∧ 43
11 ∧ 40 ∧ 43 ⇔ 11 ∧ 43
8 ∧ 23 ∧ 40 ⇔ 11 ∧ 31
8 ∧ 31 ∧ 40 ⇔ 11 ∧ 31
11 ∧ 23 ∧ 40 ⇔ 11 ∧ 31
11 ∧ 31 ∧ 40 ⇔ 11 ∧ 31
3 ∧ 14 ∧ 16 ∧ 26 ⇔ 3 ∧ 14 ∧ 16
3 ∧ 14 ∧ 16 ∧ 43 ⇔ 3 ∧ 14 ∧ 16
3 ∧ 14 ∧ 26 ∧ 43 ⇔ 3 ∧ 14 ∧ 16
3 ∧ 16 ∧ 26 ∧ 43 ⇔ 3 ∧ 14 ∧ 16
14 ∧ 16 ∧ 26 ∧ 31 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 16 ∧ 26 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 26 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 16 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 16 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 16 ∧ 31 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 31 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 26 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 26 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 26 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 26 ∧ 31 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 26 ∧ 31 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 26 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
16 ∧ 26 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
16 ∧ 26 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 26 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
16 ∧ 26 ∧ 31 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 26 ∧ 31 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 26 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
16 ∧ 23 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 23 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
16 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 23 ∧ 40 ⇔ 11 ∧ 16 ∧ 23
11 ∧ 16 ∧ 31 ∧ 40 ⇔ 11 ∧ 16 ∧ 23
8 ∧ 26 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
8 ∧ 26 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
26 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 26 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 26 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
8 ∧ 26 ∧ 31 ∧ 40 ⇔ 8 ∧ 26 ∧ 31
11 ∧ 26 ∧ 31 ∧ 40 ⇔ 8 ∧ 26 ∧ 31
8 ∧ 23 ∧ 40 ∧ 43 ⇔ 11 ∧ 43
8 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 43
11 ∧ 23 ∧ 40 ∧ 43 ⇔ 11 ∧ 43
11 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 43
3 ∧ 14 ∧ 16 ∧ 26 ∧ 43 ⇔ 3 ∧ 14 ∧ 16
14 ∧ 16 ∧ 26 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 16 ∧ 26 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 26 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 16 ∧ 26 ∧ 31 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 26 ∧ 31 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 26 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 16 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 31 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 26 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 26 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 26 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 26 ∧ 31 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
16 ∧ 26 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 26 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 26 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 26 ∧ 31 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 23 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
8 ∧ 26 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 26 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
14 ∧ 16 ∧ 26 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 26 ∧ 31 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 26 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 26 ∧ 31 ∧ 40 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 26 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 16 ∧ 26 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16
11 ∧ 14 ∧ 16 ∧ 26 ∧ 31 ∧ 40 ∧ 43 ⇔ 11 ∧ 14 ∧ 16

[Bruno Le Floch]

For what it's worth, here is the 59-node implication graph (reduced to only show implications that are not simply consequences of transitivity) displayed with Mathematica. I did not manage to control node placement much without losing the bent arrows, but perhaps with a better tool such as graphviz one can do better.
conjunctions_graph.png
conjunctions_graph.pdf
(EDIT: the graph is upside down and a couple of nodes are misplaced, I'll try to improve it.)

[Terence Tao]

Perhaps some of these data files can be uploaded to the repository (perhaps with some brief readme on how they are generated and how to interpret them)?