Equational Theories

27 Hard implications

27.1 Infinite magmas

The following forward implications can be solved by ATPs, but take unusually long:

  • 450 implies 413,426,432.

  • 463 implies 39.

  • 510 implies 439, 3862.

  • 650 implies 4.

  • 703 implies 1426,1434,4275,4307.

  • 837 implies 107.

  • 848 implies 835.

  • 1119 implies 8, 99, 151, 359, 411, 1223, 1629, 1832, 2035, 3253.

  • 1289 implies 411, 614, 1020, 2238, 2441, 2847, 3050, 4380.

  • 1312 implies 8, 411, 1020, 1629, 1832, 2035, 3253, 3319, 3862, 3915.

The following refutations required greedy methods:

  • 63 does not imply 1692.

  • 73 does not imply 99, 203, 255, 4380.

  • 118 does not imply 222, 274, 4435.

  • 124 does not imply 1924.

  • 476 does not imply 359, 3862, 4065.

  • 503 does not imply 359, 3862, 4065.

  • 511 does not imply 614, 714, 1020, 1223, 2238, 2338, 2441, 2847, 3050, 4380, 4435.

  • 677 does not imply 255.

  • 707 does not imply 1223, 1316, 2238, 2847, 2940.

  • 879 does not imply 4065.

  • 883 does not imply 2035, 2101, 2238, 2304.

  • 906 does not imply 3862.

  • 1076 does not imply 47, 99, 151, 203, 255, 411, 614, 817, 1223, 1426, 1629, 1832, 2035, 2238, 2441, 2644, 2847, 3050, 3253, 3456, 3659, 3862, 4065, 4380.

  • 1112 does not imply 8, 411, 1629, 1832, 3253, 3319, 3862, 3915.

  • 1113 does not imply 2441, 2534.

  • 1289 does not imply 3116, 4815.

  • 1648 does not imply 3253.

  • 1692 does not imply 47, 1832, 2441, 3050, 3456, 4065.

The following refutations required ad hoc methods:

  • 1447 does not imply 1429, 4269.

  • 206 does not imply 1648.

  • 1648 does not imply 206.

Here is a list of the final implications to refute that required analysis in the project:

Three-variable equations:

  • 1485 does not imply 151, 3456, 3862.

  • 854 does not imply 413, 1045, 1055, 3316, 3925.

  • 1117 does not imply 2441.

  • 1437 does not imply 4269.

The “Hardy–Ramanujan cluster”

  • 917 does not imply 1629, 1729, 2441, 2541.

  • 1323 does not imply 2744.

  • 1526 does not imply 1223, 2744.

  • 1729 does not imply 817, 917.

  • 2541 does not imply 1729.

  • 2744 does not imply 1323, 1526.

Other two-variable equations:

  • 1722 does not imply 644, 3050, 1832.

  • 1516 does not imply 255.

  • 1518 does not imply 47, 614, 817, 3862.

  • 3308 does not imply 3456.

  • 3342 does not imply 3456, 3522, 4065, 4118.

  • 3352 does not imply 4065.

  • 3475 does not imply 3659.

27.2 Finite magmas

In the case of finite magmas, there are some non-trivial positive implications:

There are also some tricky negative implications:

  • 476 does not imply 359, 4065.

  • 503 does not imply 4065, 3862.

  • 854 does not imply 107, 1248, 1251.

  • 1076 does not imply 2234, 2294, 4435.

  • 1518 does not imply 47, 817.

  • 3352 does not imply 4065.

  • 3475 does not imply 3659.

Finally, we have some open questions:

  • Does 677 imply 255?

  • Does 13102 have a non-trivial finite model?