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.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.