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.

• Middle Bol => all 10 sv-instances of aa1

Proof: (in, out, pf, xml)

This is a single proof of the conjunction of the 10 goals.

• Middle Bol + 10 sv-instances of aa1 => all 10 sv-instances of aa2

Proof: (in, out, pf, xml)

This is a single proof of the conjunction of the 10 goals.

• Middle Bol + 10 sv-instances of aa1 => all 10 sv-instances of aa3

Proof: (in, out, pf, xml)

This is a single proof of the conjunction of the 10 goals.

• Middle Bol => all 30 sv-instances of the aa goals

Proof: (in, out, pf, xml)

This is a single proof of the conjunction of the 30 goals.

### Results posted through July 23, 2022

• aK1
```      status : proved with no lemmas
```
aK1.pf

• all 30 instances of the 3 aa goals by renaming a single variable
```      status : proved with lemmas
lemmas : 4 single-a goals
posted AIM lemmas
cb100 lemmas
```
30instances.goals
30instances.pf_1 (large file)

Eliminating the cb100 lemmas,

```      status : proved with lemmas
lemmas : 4 single-a goals
posted AIM lemmas
```
30instances.pf_2 (large file)

Sfdf derivations from axioms of some of the 30 instances:

aa1{x1/x2}: (in, out, pf, xml)

aa1{x1/x4}: (in, out, pf, xml)

aa1{x1/x5}: (in, out, pf, xml)

aa2{x1/x2}: (in, out, pf, xml)

aa3{x1/x2}: (in, out, pf, xml)

aa3{x1/x5}: (in, out, pf, xml)

aa3{x4/x5}: (in, out, pf, xml)

• permutations of aa3 in aa1_eq_aa3 and aa2_eq_aa3
```      status : 120/240 proved with lemmas (60/120 permutations of each)
lemmas : 4 single-a goals
nil3 clauses
instances of the aa goals by renaming a single variable
posted AIM lemmas
cb100 lemmas
```
120aaeq.goals
120aaeq.pf (large file)

Note that the aa1_eq_aa2 case is implied.

• permutations of the aa goals
```      status : proved 180 with lemmas (60/120 permutations of each)
lemmas : permutations of aa1_eq_aa3 and aa2_eq_aa3
```
120aaeq.sos
180aaperms.goals
180aaperms.pf

• nilpotency class 3

The current status is that there is a high-level mathematical argument that AIM loops are nilpotent of class 3, but we do not yet have a Prover9 proof. An intermediate goal is to prove it assuming middle Bol as an extra assumption.

We know from posted lemmas that middle Bol => the 23/32 nil3 clauses having at least one occurrence of K. It remains to prove the 9/32 having 0 occurrences of K.

Here is a proof that it suffices to prove just one of the 9, for example,

```      a(a(a(x,y,z),u,w),v5,v6) = 1   # label("nil3 24, aa1-Nl").
```
Proof: (in, out, pf, xml)

### Some remaining challenges

• Prove any of 120/240 missing permutations of aa1_eq_aa3 and aa2_eq_aa3

• Prove any of 180/360 missing permutations of the 3 aa goals.

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.