AIM + Middle Bol
x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").

July 2022

Results posted after July 23, 2022

See also Michael Kinyon's AIM Problem Again page. Hints from those results were used to help find the results posted here.

In the followng, "sv-instances" refers to single-variable instances, that is, instances formed by renaming a single variable.

Results posted through July 23, 2022

Some remaining challenges

Here, for example, are the 60/120 missing permutations of aa1_eq_aa3.

Note that assuming, for example, the single clause

   a(a(x,y,z),u,w) = a(x,y,a(z,w,u)) # label("aa1_eq_aa3 (12354)").
suffices to prove the remaining 59/60. It also suffices to prove all 360 aa permutations.