AIM Project

June 2021


Main Conjecture: AIM => {Ka,aK1,aK2,aK3,aa1,aa2,aa3}

The results presented here rely on the following clause representation of AIM,
formulas(assumptions).

   % loop axioms
   1 * x = x.
   x * 1 = x.
   x \ (x * y) = y.
   x * (x \ y) = y.
   (x * y) / y = x.
   (x / y) * y = x.

   % associator (right associated * a = left associated)
   (x * (y * z)) \ ((x * y) * z) = a(x,y,z) # label("associator").

   % commutator ( (x * y) * K(y,x) = y * x )
   (x * y) \ (y * x) = K(y,x) # label("commutator").

   % inner mappings
   (y * x) \ (y * (x * u)) = L(u,x,y).
   ((u * x) * y) / (x * y) = R(u,x,y).
   x \ (u * x) = T(u,x).

   % abelian inner mapping group
   T(T(u,x),y) = T(T(u,y),x).
   T(L(u,x,y),z) = L(T(u,z),x,y).
   T(R(u,x,y),z) = R(T(u,z),x,y).
   L(R(u,x,y),z,w) = R(L(u,z,w),x,y).
   L(L(u,x,y),z,w) = L(L(u,z,w),x,y).
   R(R(u,x,y),z,w) = R(R(u,z,w),x,y).

end_of_list.
and the following representation of the 7 goals.
formulas(goals).

   K(a(x,y,z),u) = 1     # label("Ka").
   a(K(x,y),z,u) = 1     # label("aK1").
   a(x,K(y,z),u) = 1     # label("aK2").
   a(x,y,K(z,u)) = 1     # label("aK3").

   a(a(x,y,z),u,w) = 1   # label("aa1").
   a(x,a(y,z,u),w) = 1   # label("aa2").
   a(x,y,a(z,u,w)) = 1   # label("aa3").

end_of_list.

Including lemmas such as the following as additional input assumptions can help with some searches.

formulas(assumptions).

   % cancellation laws (long form)

   x * y != u | x * z != u | y = z # label("*-Cancellation 1").
   y * x != u | z * x != u | y = z # label("*-Cancellation 2").

   x / y != u | x / z != u | y = z # label("/-Cancellation 1").
   y / x != u | z / x != u | y = z # label("/-Cancellation 2").

   x \ y != u | x \ z != u | y = z # label("\-Cancellation 1").
   y \ x != u | z \ x != u | y = z # label("\-Cancellation 2").

   T(x,y) != u | T(z,y) != u | x = z # label("T-Cancellation 1").
   L(z,x,y) != u | L(w,x,y) != u | z = w # label("L-Cancellation 1").
   R(z,x,y) != u | R(w,x,y) != u | z = w # label("R-Cancellation 1").

   % cancellation laws (short form)

   x * y != x * z | y = z # label("*-Cancellation 3").
   y * x != z * x | y = z # label("*-Cancellation 4").

   x / y != x / z | y = z # label("/-Cancellation 3").
   y / x != z / x | y = z # label("/-Cancellation 4").

   x \ y != x \ z | y = z # label("\-Cancellation 3").
   y \ x != z \ x | y = z # label("\-Cancellation 4").

   T(x,y) != T(z,y) | x = z # label("T-Cancellation 2").
   L(z,x,y) != L(w,x,y) | z = w # label("L-Cancellation 2").
   R(z,x,y) != R(w,x,y) | z = w # label("R-Cancellation 2").

   % sometimes helpful for demodulation-free proofs

   x != y | x * z = y * z # label("Aux 1").
   x != y | z * x = z * y # label("Aux 2").
   x != y | x / z = y / z # label("Aux 3").
   x != y | z / x = z / y # label("Aux 4").
   x != y | x \ z = y \ z # label("Aux 5").
   x != y | z \ x = z \ y # label("Aux 6").

   x != y | y != z | x = z # label("Transitivity =").

end_of_list.
In addition to the results posted here, Michael Kinyon has a page, AIM Problem Again, for proofs in which all derived (non input) clauses are units. He also has a page on AIM-TT, a generalization of the AIM problem that is identical to AIM except that it omits the axiom
   T(T(u,x),y) = T(T(u,y),x).

Result 1: Equivalence of {Ka,aK1,aK2,aK3}

Result 2: Equivalence of {aa1,aa2,aa3}

Result 3: More results relating {Ka,aK1,aK2,aK3}

   a(K(x,y),z,u) = a(x,z,K(u,y)) # label("aK1_eq_aK3").
(in, out, pf, xml)
   K(a(x,y,z),u) = a(x,y,K(z,u)) # label("Ka_eq_aK3").
(in, out, pf, xml)
   K(a(x,y,z),u) = K(x,a(u,y,z)) # label("Ka1_eq_Ka2").
(in, out, pf, xml)
   a(x,K(y,z),u) = a(u,K(z,y),x) # label("aK2rev").
(in, out, pf, xml)

A result for aK2 analogous to aK1_eq_aK3 and Ka_eq_aK3 remains open. Several special cases are covered in the Miscellaneous Results section below.

Result 4: Some properties of a and K

   K(x,y) * a(u,v,w) = a(u,v,w) * K(x,y) # label("aKcom").
(in, out, pf, xml)
   K(K(x,y),z) = K(x,K(y,z))         # label("Kassoc").
   K(x,K(y,z)) = K(y,K(x,z))         # label("KKcom_a").
   K(x,K(y,z)) = K(x,K(z,y))         # label("KKcom_b").
   K(x,y) * K(z,u) = K(z,u) * K(x,y) # label("KKcom_c").
   K(x,y) * K(y,x) = 1               # label("KxyKyx").
   K(K(x,y),K(z,u)) = 1              # label("KofKK").
   K(x,y) = (x * y) / (y * x)        # label("K-dual").
(in, out, pf, xml)
   K(x,y) = x \ T(x,y)               # label("K_eq_T_a").
   K(x,y) = y / T(y,x)               # label("K_eq_T_b").
   K(T(x,y),T(z,y)) = K(x,z)         # label("K_eq_T_c").
(in, out, pf, xml)
   K(x,K(y,z * z)) = 1               # label("Ksqmap"). 
(in, out, pf, xml)

Result 5: Some properties of T, L and R

   1 / (1 / T(x,y)) = T(1 / (1 / x),y)     # label("T property").
   1 / (1 / L(x,y,z)) = L(1 / (1 / x),y,z) # label("L property").
   1 / (1 / R(x,y,z)) = R(1 / (1 / x),y,z) # label("R property").

   K(x \ 1,x) = K(T(x,y) \ 1,T(x,y))       # label("KinvT").
   K(x \ 1,x) = K(L(x,y,z) \ 1,L(x,y,z))   # label("KinvL").
   K(x \ 1,x) = K(R(x,y,z) \ 1,R(x,y,z))   # label("KinvR").
(in, out, pf, xml)
   K(x,R(y,z,u)) = K(x,L(y,z,u))           # label("KRKL").
   T(x,R(y,z,u)) = T(x,L(y,z,u))           # label("TRTL").
   R(K(x,y),z,u) = L(K(x,y),z,u)           # label("RKLK 1").
   R(x,K(y,z),u) = L(x,K(y,z),u)           # label("RKLK 2").
   R(x,y,K(z,u)) = L(x,y,K(z,u))           # label("RKLK 3").
   L(K(x,y),z,u) = K(x,L(y,z,u))           # label("LKKL").
(in, out, pf, xml)

Result 6: Instances of {Ka,aK1,aK2,aK3}

%  a(K(w,x),y,z) = 1  *** original goal ***
   a(K(w,w),y,z) = 1 # label("aK1{x1/x2}").
   a(K(w,x),w,z) = 1 # label("aK1{x1/x3}").
   a(K(w,x),y,w) = 1 # label("aK1{x1/x4}").
   a(K(w,x),x,z) = 1 # label("aK1{x2/x3}").
   a(K(w,x),y,x) = 1 # label("aK1{x2/x4}").
   a(K(w,x),y,y) = 1 # label("aK1{x3/x4}").

%  a(w,K(x,y),z) = 1  *** original goal ***
   a(w,K(w,y),z) = 1 # label("aK2{x1/x2}").
   a(w,K(x,w),z) = 1 # label("aK2{x1/x3}").
   a(w,K(x,y),w) = 1 # label("aK2{x1/x4}").
   a(w,K(x,x),z) = 1 # label("aK2{x2/x3}").
   a(w,K(x,y),x) = 1 # label("aK2{x2/x4}").
   a(w,K(x,y),y) = 1 # label("aK2{x3/x4}").

%  a(w,x,K(y,z)) = 1  *** original goal ***
   a(w,w,K(y,z)) = 1 # label("aK3{x1/x2}").
   a(w,x,K(w,z)) = 1 # label("aK3{x1/x3}").
   a(w,x,K(y,w)) = 1 # label("aK3{x1/x4}").
   a(w,x,K(x,z)) = 1 # label("aK3{x2/x3}").
   a(w,x,K(y,x)) = 1 # label("aK3{x2/x4}").
   a(w,x,K(y,y)) = 1 # label("aK3{x3/x4}").

%  K(a(w,x,y),z) = 1  *** original goal ***
   K(a(w,w,y),z) = 1 # label("Ka{x1/x2}").
   K(a(w,x,w),z) = 1 # label("Ka{x1/x3}").
   K(a(w,x,y),w) = 1 # label("Ka{x1/x4}").
   K(a(w,x,x),z) = 1 # label("Ka{x2/x3}").
   K(a(w,x,y),x) = 1 # label("Ka{x2/x4}").
   K(a(w,x,y),y) = 1 # label("Ka{x3/x4}").

These are the 24 proper instances of {Ka,aK1,aK2,aK3} formed by renaming a single variable.

(in, out, pf, xml)

Result 7: Instances of {aa1,aa2,aa3}

   a(a(x,y,x),u,w) = 1 # label("aa1{x1/x3}").
   a(x,a(y,z,u),x) = 1 # label("aa2{x1/x5}").
   a(x,a(y,z,y),w) = 1 # label("aa2{x2/x4}").
   a(x,y,a(z,u,z)) = 1 # label("aa3{x3/x5}").

These are 4 of the 30 proper instances of {aa1,aa2,aa3} formed by renaming a single variable.

(in, out, pf, xml)

Result 8: Nilpotency class 3 properties

Michael Kinyon originally presented 32 properties sufficient to prove that AIM loops are nilpotent of class 3. Of these 32,
1 has 3 occurrences of K
7 have 2 occurrences of K
15 have 1 occurrence of K
9 have 0 occurrences of K
Nil3 Result 1

Proofs of the 8 of 32 having > 1 occurrence of K.

   K(x,K(y,K(z,u))) = 1    # label("nil3 1, KK-C").
   K(K(x,a(y,z,u)),w) = 1  # label("nil3 2, Ka-C").
   K(a(K(x,y),z,u),w) = 1  # label("nil3 3, aK1-C").
   K(a(x,K(y,z),u),w) = 1  # label("nil3 4, aK2-C").
   K(a(x,y,K(z,u)),w) = 1  # label("nil3 5, aK3-C").
   a(K(x,K(y,z)),u,w) = 1  # label("nil3 9, KK-Nl").
   a(x,K(y,K(z,u)),w) = 1  # label("nil3 10, KK-Nm").
   a(x,y,K(z,K(u,w))) = 1  # label("nil3 11, KK-Nr").
(in, out, pf, xml)
Nil3 Result 2

{7,15,18} => the remaining 12 of 15 having exactly 1 occurrence of K

Extra assumptions:

   K(a(x,a(y,z,u),w),v5) = 1 # label("nil3 7, aa2-C").
   a(a(K(x,y),z,u),w,v5) = 1 # label("nil3 15, aK1-Nl").
   a(x,a(K(y,z),u,w),v5) = 1 # label("nil3 18, aK1-Nm").
12 goals:
   K(a(a(x,y,z),u,w),v5) = 1   # label("nil3 6, aa1-C").
%  K(a(x,a(y,z,u),w),v5) = 1   # label("nil3 7, aa2-C").
   K(a(x,y,a(z,u,w)),v5) = 1   # label("nil3 8, aa3-C").
   a(K(x,a(y,z,u)),w,v5) = 1   # label("nil3 12, Ka-Nl").
   a(x,K(y,a(z,u,w)),v5) = 1   # label("nil3 13, Ka-Nm").
   a(x,y,K(z,a(u,w,v5))) = 1   # label("nil3 14, Ka-Nr").
%  a(a(K(x,y),z,u),w,v5) = 1   # label("nil3 15, aK1-Nl").
   a(a(x,K(y,z),u),w,v5) = 1   # label("nil3 16, aK2-Nl").
   a(a(x,y,K(z,u)),w,v5) = 1   # label("nil3 17, aK3-Nl").
%  a(x,a(K(y,z),u,w),v5) = 1   # label("nil3 18, aK1-Nm").
   a(x,a(y,K(z,u),w),v5) = 1   # label("nil3 19, aK2-Nm").
   a(x,a(y,z,K(u,w)),v5) = 1   # label("nil3 20, aK3-Nm").
   a(x,y,a(K(z,u),w,v5)) = 1   # label("nil3 21, aK1-Nr").
   a(x,y,a(z,K(u,w),v5)) = 1   # label("nil3 22, aK2-Nr").
   a(x,y,a(z,u,K(w,v5))) = 1   # label("nil3 23, aK3-Nr").
(in, out, pf, xml)
Nil3 Result 3

nil3 15 => nil3 7

Extra assumption:

   a(a(K(x,y),z,u),w,v5) = 1 # label("nil3 15, aK1-Nl").
Goal:
   K(a(x,a(y,z,u),w),v5) = 1 # label("nil3 7, aa2-C").
(in, out, pf, xml)
Nil3 Result 4

{15,18} => the remaining 13 of 15 having exactly 1 occurrence of K

Extra assumptions:

   a(a(K(x,y),z,u),w,v5) = 1 # label("nil3 15, aK1-Nl").
   a(x,a(K(y,z),u,w),v5) = 1 # label("nil3 18, aK1-Nm").
13 goals:
   K(a(a(x,y,z),u,w),v5) = 1   # label("nil3 6, aa1-C").
   K(a(x,a(y,z,u),w),v5) = 1   # label("nil3 7, aa2-C").
   K(a(x,y,a(z,u,w)),v5) = 1   # label("nil3 8, aa3-C").
   a(K(x,a(y,z,u)),w,v5) = 1   # label("nil3 12, Ka-Nl").
   a(x,K(y,a(z,u,w)),v5) = 1   # label("nil3 13, Ka-Nm").
   a(x,y,K(z,a(u,w,v5))) = 1   # label("nil3 14, Ka-Nr").
%  a(a(K(x,y),z,u),w,v5) = 1   # label("nil3 15, aK1-Nl").
   a(a(x,K(y,z),u),w,v5) = 1   # label("nil3 16, aK2-Nl").
   a(a(x,y,K(z,u)),w,v5) = 1   # label("nil3 17, aK3-Nl").
%  a(x,a(K(y,z),u,w),v5) = 1   # label("nil3 18, aK1-Nm").
   a(x,a(y,K(z,u),w),v5) = 1   # label("nil3 19, aK2-Nm").
   a(x,a(y,z,K(u,w)),v5) = 1   # label("nil3 20, aK3-Nm").
   a(x,y,a(K(z,u),w,v5)) = 1   # label("nil3 21, aK1-Nr").
   a(x,y,a(z,K(u,w),v5)) = 1   # label("nil3 22, aK2-Nr").
   a(x,y,a(z,u,K(w,v5))) = 1   # label("nil3 23, aK3-Nr").
(in, out, pf, xml)

In addition to the results presented here, Michael Kinyon has a page on nil3. It includes a list of known dependencies among the 32.

Result 9: Nilpotency class 4 properties

Here are 128 nilpotency class 4 properties derived from the 32 original nil3 properties. Many of the 128 follow simply from known nil3 properties and dependencies among the nil3 properties. This section includes nil4 results that appear (for now) to be more significant.

Goal:

   K(a(x,a(y,K(z,u),w),v5),v6) = 1 # label("nil4 19K").
nil4 19K: (in, out, pf, xml)

The Conjecture

We prove the main conjecture for various special cases, that is, for AIM extended with extra assumptions.

Note that by Results 1 and 2 above, it suffices to show any one of {Ka,aK1,aK2,aK3} and any one of {aa1,aa2,aa3}.

Case 1: Moufang

   ((x * y) * x) * z = x * (y * (x * z)) # label("Moufang").
Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 2: LC

   (x * (x * y)) * z = x * (x * (y * z)) # label("LC").
Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 3: left Bol

   (x * (y * x)) * z = x * (y * (x * z)) # label("left Bol").
Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 4: RIF + LIP

   ((x * (y * z)) * x) * y = (x * y) * (z * (x * y)) # label("RIF").

   (1 / x) * (x * y) = y # label("LIP").
Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 5: L1-distributivity

   L(x1,y,z) * L(x2,y,z) = L(x1 * x2,y,z) # label("L1dist").
Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 6: R1-distributivity

   R(x1,y,z) * R(x2,y,z) = R(x1 * x2,y,z) # label("R1dist").
Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 7: generalized Moufang

   ((1 / x) \ y) * (z * x) = x * ((y * z) * x) # label("Osborn").
   x * ((y * x) \ 1) = y \ 1 # label("WIP").
Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 8: generalized Bol

   (x * (y * x)) * ((1 / x) * z) = x * (y * z) # label("gen left Bol").
   (x * (y \ 1)) * ((y * z) * y) = (x * z) * y # label("gen right Bol").
Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

Case 9: LCC

   ((x * y) / x) * (x * z) = x * (y * z) # label(LCC).
This result was already known when we began the AIM project.

Proof of aK1: (in, out, pf, xml)

Proof of aa1: (in, out, pf, xml)

In addition to the 7 primary goals, this case also includes a proof of KK.

   K(K(x,y),z) = 1 # label("KK").

Proof of KK: (in, out, pf, xml)

Case 10: Nuclear Squares

   (x * x) * (y * z) = ((x * x) * y) * z # label("NucSq_l").
   (x * (y * y)) * z = x * ((y * y) * z) # label("NucSq_m").
   (x * y) * (z * z) = x * (y * (z * z)) # label("NucSq_r").

This case is in progress.

Proof of aK1: (in, out, pf, xml)

A proof of {aa1,aa2,aa3} remains open.

Case 11: T1-distributivity

   T(x,y) * T(z,y) = T(x * z,y) # label("T1dist").

This case is in progress.

Proof of aK1: (in, out, pf, xml)

A proof of {aa1,aa2,aa3} remains open.

Case 12: middle Bol + KK => aK1

Extra assumptions:

   x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").
   K(K(x,y),z) = 1                       # label("KK").
Proof of aK1: (in, out, pf, xml)

A proof of {aa1,aa2,aa3} remains open.

Case 13: middle Bol => aK1

Extra assumption:
   x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").
Proof of aK1: (in, out, pf, xml)

A proof of {aa1,aa2,aa3} remains open.

Miscellaneous Results

This section includes results that might be useful or interesting but don't fit in the previous two sections. Typically these will be intermediate results that (hopefully) will eventually get replaced by stronger results in the previous sections.

Misc 1: Relating aK2 to aK3 with various extra assumptions

Note that the different cases may have different permutations of the variables in the goal clause.

Note also that rather than showing an equality between aK2 and aK3 for some permutation of the variables, it suffices to show that every instance of aK2 is equal to some instance of aK3 and every instance of aK3 is equal to some instance of aK2.

Case 1
Goal clause:
   a(x,K(y,z),u) = a(y,u,K(x,z)) # label("aK2_eq_aK3 (2413)").
Extra assumption:
   a(a(x,y,z),z,u) = 1 # label("aa1{x3/x4}").
(in, out, pf, xml)
Case 2
Goal clause:
   a(x,K(y,z),u) = a(y,x,K(z,u)) # label("aK2_eq_aK3 (2134)").
Extra assumption:
   a(a(x,y,z),u,w) = a(a(x,y,u),z,w) # label("aa1_34").
(in, out, pf, xml)
Case 3
Goal clause:
   a(x,K(y,z),u) = a(u,x,K(y,z)) # label("aK2_eq_aK3 (4123)").
Extra assumption:
   a(x,a(y,z,u),u) = 1 # label("aa2{x4/x5}").
(in, out, pf, xml)
Case 4
Goal clause:
   a(x,K(y,z),u) = a(y,u,K(x,z)) # label("aK2_eq_aK3 (2413)").
Extra assumption:
   a(x,y,a(y,z,u)) = 1 # label("aa3{x2/x3}").
(in, out, pf, xml)
Case 5
Goal clause:
   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3 (1243)").
Extra assumption:
   ((1 / x) \ y) * (z * x) = x * ((y * z) * x) # label("Osborn").
(in, out, pf, xml)
Case 6
Goal clause:
   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3 (1243)").
Extra assumption:
   x * ((y * x) \ 1) = y \ 1 # label("WIP").
(in, out, pf, xml)
Case 7
Goal clause:
   a(x,K(y,z),u) = a(y,z,K(u,x)) # label("aK2_eq_aK3 (2341)").
Extra assumption:
   ((x * y) \ 1) * ((x \ 1) \ 1) = y \ 1 # label("DWIP").
(in, out, pf, xml)
Case 8
Goal clause:
   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3 (1243)").
Extra assumption:
   (1 / x) * (x * y) = y # label("LIP").
(in, out, pf, xml)
Case 9
Goal clause:
   a(x,K(y,z),u) = a(y,u,K(z,x)) # label("aK2_eq_aK3 (2431)").
Extra assumption:
   T(T(x,y),y) = x # label("imord2 T").
(in, out, pf, xml)
It follows that
   K(x,y) = K(y,x) # label("Kcom").
also suffices for permutation 2431, since it is easily shown to be equivalent to imord2 T in AIM.
Case 10
Goal clause:
   a(x,K(y,z),u) = a(y,u,K(z,x)) # label("aK2_eq_aK3 (2431)").
Extra assumption:
   K(x,y) = K(y,x) # label("Kcom").
(in, out, pf, xml)
Case 11
Goal clause:
   a(x,K(y,z),u) = a(u,x,K(y,z)) # label("aK2_eq_aK3 (4123)").
Extra assumptions:
   a(a(x,y,z),u,x) = 1 # label("aa1{x1/x5}").
   a(a(x,y,z),u,w) = a(a(x,y,z),w,u) # label("aa1_45").
(in, out, pf, xml)
Case 12
Goal clause:
   a(x,K(y,z),u) = a(y,z,K(u,x)) # label("aK2_eq_aK3 (2341)").
Extra assumption:
   a(a(x,y,z),u,w) = a(a(x,y,z),w,u) # label("aa1_45").
(in, out, pf, xml)
Case 13
Goal clause:
   a(x,K(y,z),u) = a(y,u,K(x,z)) # label("aK2_eq_aK3 (2413)").
Extra assumption:
   a(a(x,y,z),u,w) = 1   # label("aa1").
(in, out, pf, xml)

The extra assumption of Case 12, clause aa1_45, is a trivial consequence of aa1, but this result is for a different permutation of aK2_eq_aK3.

Case 14
Goal clause:
   a(x,K(y,z),u) = a(y,z,K(u,x)) # label("aK2_eq_aK3 (2341)").
Extra assumption:
   ((x * (y * z)) * x) * y = (x * y) * (z * (x * y)) # label("RIF").
(in, out, pf, xml)
Case 15
Goal clause:
   a(x,K(y,z),u) = a(x,u,K(y,z)) # label("aK2_eq_aK3 (1423)").
Extra assumptions:
   % nuclear squares
   (x * x) * (y * z) = ((x * x) * y) * z # label("NucSq_l").
   (x * (y * y)) * z = x * ((y * y) * z) # label("NucSq_m").
   (x * y) * (z * z) = x * (y * (z * z)) # label("NucSq_r").
(in, out, pf, xml)
Here is a units-only derivation of
   a(x * y,y,K(z,u)) = a(x,K(u,z),y).
Rather than showing an equality between aK2 and aK3 for some permutation of the variables, this says that every instance of aK2 is equal to an instance of aK3. Substituting w/y for x and simplifying yields
   a(w,y,K(z,u)) = a(w/y,K(u,z),y).
which says that every instance of aK3 is equal to an instance of aK2.
Case 16
Goal clauses:

   a(x,y,K(y * z,u)) = a(y,K(u,x),z) # label("aK2_eq_aK3").
   a(x,y,K(w,u)) = a(y,K(u,x),y \ w) # label("aK2_eq_aK3").

Extra assumption:

   % automorphic inverse property (AIP)
   (1 / x) * (1 / y) = 1 / (x * y) # label("AIP").
(in, out, pf, xml)
The proof was initially found by running with different lexical orderings, accumulating partial results along the way. The proof was found at the 10th iteration, with results from 4 of the 9 previous orderings contributing to the proof.
Case 17
Goal clause:

   a(x,K(y,z),u) = a(z,y,K(x,u)) # label("aK2_eq_aK3 (3214)").

Extra assumption:

   % automorphic inverse property (AIP)
   (1 / x) * (1 / y) = 1 / (x * y) # label("AIP").
(in, out, pf, xml)

AIP is covered in Case 16, but this version is for a nicer goal.

Case 18

Goal clause:

   a(x,K(y,z),u) = a(x,y,K(u,z)) # label("aK2_eq_aK3 (1243)").

Extra assumptions:

   (x * y) * x = x * (y * x) # label("flex").
(in, out, pf, xml)
Case 19
Goal clause:

   a(x,K(y,z),u) = a(x,z,K(y,u)) # label("aK2_eq_aK3 (1324)").

Extra assumption:

   % antiautomorphic inverse property (AAIP)
   (1 / x) * (1 / y) = 1 / (y * x) # label("AAIP").

Done but being cleaned up for posting ...

Misc 2: A proper instance of aK3 suffices to prove aK3

Extra assumption:
   a(x,y * ((L(z,y,x) \ 1) \ T((L(z,y,x) \ 1) * z,u)),K(u,L(z,y,x) \ 1)) = 1 # label("aK3 instance").
(in, out, pf, xml)

Misc 3: generalized Bol => Osborn

   (x * (y * x)) * ((1 / x) * z) = x * (y * z) # label("gen left Bol").
   (x * (y \ 1)) * ((y * z) * y) = (x * z) * y # label("gen right Bol").

   ((1 / x) \ y) * (z * x) = x * ((y * z) * x) # label("Osborn 1").
   (x * y) * (z / (x \ 1)) = (x * (y * z)) * x # label("Osborn 2").
   (1 / x) \ (((1 / x) * y) * z) = (y * (z * x)) / x # label("Osborn 3").
   x \ ((x * y) * z) = (y * (z * (x \ 1))) / (x \ 1) # label("Osborn 4").
Proof: (in, out, pf, xml)

The 4 versions of the Osborn condition are equivalent, but all 4 are included as goals here for the additional hints taken from the proofs.

Misc 4: Three proper instances of aa1 suffice to prove aa2

Extra assumptions:
   a(a(x,1 / T(y,z * w),u),(((a(x,1 / T(y,z * w),u) \ ((x * ((1 / T(y,z * w)) * u)) \ (x * u))) * z) * w) / (z * w),z * w) = 1 # label("aa1_1").

   a(a(x,1 / T(y,z * w),u),a(x,1 / T(y,z * w),u) \ ((x * ((1 / T(y,z * w)) * u)) \ (x * u)),z) = 1 # label("aa1_2").

   a(a(x,1 / T(y,z * w),u),(a(x,1 / T(y,z * w),u) \ ((x * ((1 / T(y,z * w)) * u)) \ (x * u))) * z,w) = 1 # label("aa1_3").
(in, out, pf, xml)

Misc 5: All 32 nil3 clauses assuming 2 extra assumptions

Extra assumptions:
   a(a(x,y,z),u,x) = 1 # label("aa1{x1/x5}").
   a(a(x,y,z),u,w) = a(a(x,y,z),w,u) # label("aa1_45").
Proofs 1-23

Proofs 24-32

Misc 6: Other results with extra assumption aa1_45

Extra assumption:
   a(a(x,y,z),u,w) = a(a(x,y,z),w,u) # label("aa1_45").
Case 1
aa1_45 => nil3 {7,15,18}
   K(a(x,a(y,z,u),w),v5) = 1 # label("nil3 7, aa2-C").
   a(a(K(x,y),z,u),w,v5) = 1 # label("nil3 15, aK1-Nl").
   a(x,a(K(y,z),u,w),v5) = 1 # label("nil3 18, aK1-Nm").
nil3 7: (in, out, pf, xml)
nil3 15: (in, out, pf, xml)
nil3 18: (in, out, pf, xml)
Case 2
aa1_45 => all 15 of the 32 original nil3 properties having exactly 1 occurrence of K
(in, out, pf, xml)
This combines the following posted nil3 results.
aa1_45 => nil3 15

aa1_45 => nil3 18

nil3 {15,18} => the remaining 13 having exactly 1 occurrence of K

Case 3
aa1_45 => all 9 of the 32 original nil3 properties having 0 occurrences of K
   a(a(a(x,y,z),u,w),v5,v6) = 1 # label("nil3 24, aa1-Nl").
   a(a(x,a(y,z,u),w),v5,v6) = 1 # label("nil3 25, aa2-Nl").
   a(a(x,y,a(z,u,w)),v5,v6) = 1 # label("nil3 26, aa3-Nl").
   a(x,a(a(y,z,u),w,v5),v6) = 1 # label("nil3 27, aa1-Nm").
   a(x,a(y,a(z,u,w),v5),v6) = 1 # label("nil3 28, aa2-Nm").
   a(x,a(y,z,a(u,w,v5)),v6) = 1 # label("nil3 29, aa3-Nm").
   a(x,y,a(a(z,u,w),v5,v6)) = 1 # label("nil3 30, aa1-Nr").
   a(x,y,a(z,a(u,w,v5),v6)) = 1 # label("nil3 31, aa2-Nr").
   a(x,y,a(z,u,a(w,v5,v6))) = 1 # label("nil3 32, aa3-Nr").
nil3 24: (in, out, pf, xml)
nil3 25: (in, out, pf, xml)
nil3 26: (in, out, pf, xml)
nil3 27: (in, out, pf, xml)
nil3 28: (in, out, pf, xml)
nil3 29: (in, out, pf, xml)
nil3 30: (in, out, pf, xml)
nil3 31: (in, out, pf, xml)
nil3 32: (in, out, pf, xml)
Comment
aa1_45 => all 32 of the original nil3 properties

This follows from the following posted results.

All 8 of the 32 nil3 properties having > 1 occurrence of K are AIM lemmas.

aa1_45 => all 15 of the 32 nil3 properties having exactly 1 occurrence of K

aa1_45 => all 9 of the 32 nil3 properties having 0 occurrences of K (each posted separately)

Combining the 32 proofs in a single run: (in, out, pf, xml)

It follows that in order to prove that AIM loops are nilpotent of class 3, it suffices to prove any one of {aa1,aa2,aa3}.

Case 4
aa1_45 + aK1 => aa1

Additional extra assumption:

   a(K(x,y),z,u) = 1 # label("aK1").
Proved clause:
   a(a(x,y,z),u,w) = 1 # label("aa1").
(in, out, pf, xml)
It follows that in order to prove the primary AIM conjecture, it suffices to prove any one of {Ka,aK1,aK2,aK3} and aa1_45.

Misc 6: AIM loops are nilpotent of class at most 3

This result relies on a high-level mathematical argument that makes use of the following Prover9 lemmas. To complete the proof with Prover9, it will suffice, for example, to prove that middle Bol + KK => aa1.

In addition to the results posted here, Michael Kinyon has a page here.

Part 1: middle Bol + KK => 6 instances of the aa goals

Extra assumptions:

   x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").
   K(K(x,y),z) = 1                       # label("KK").
Proved clauses:
   a(a(x,x,z),u,w) = 1 # label("aa1{x1/x2}").
   a(a(x,y,y),u,w) = 1 # label("aa1{x2/x3}").
   a(x,a(y,y,u),w) = 1 # label("aa2{x2/x3}").
   a(x,a(y,z,z),w) = 1 # label("aa2{x3/x4}").
   a(x,y,a(z,z,w)) = 1 # label("aa3{x3/x4}").
   a(x,y,a(z,u,u)) = 1 # label("aa3{x4/x5}").
(in, out, pf, xml)
Part 2: middle Bol + KK + 6 instances of the aa goals => Ka

Extra assumptions:

   x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").
   K(K(x,y),z) = 1                       # label("KK").

   a(a(x,x,z),u,w) = 1 # label("aa1{x1/x2}").
   a(a(x,y,y),u,w) = 1 # label("aa1{x2/x3}").
   a(x,a(y,y,u),w) = 1 # label("aa2{x2/x3}").
   a(x,a(y,z,z),w) = 1 # label("aa2{x3/x4}").
   a(x,y,a(z,z,w)) = 1 # label("aa3{x3/x4}").
   a(x,y,a(z,u,u)) = 1 # label("aa3{x4/x5}").
Proved clause:
   K(a(x,y,z),u) = 1 # label("Ka").
(in, out, pf, xml)
Combining results: middle Bol + KK => aK1

Extra assumptions:

   x * ((y * z) \ x) = (x / z) * (y \ x) # label("middle Bol").
   K(K(x,y),z) = 1                       # label("KK").
Proved clause:
   a(K(x,y),z,u) = 1     # label("aK1").
(in, out, pf, xml)

This work was supported in part by the AI4REASON ERC Consolidator grant nr. 649043, the Czech project AI&Reasoning CZ.02.1.01/0.0/0.0/15_003/0000466 and the European Regional Development Fund.