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

November 2021


Results

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.