A certified basis of 25 identities
This list of identities is a basis, proved in Lean, of [6, 11311], which generates the variety V[11311]. Removing the identities that follow from the others leaves 5 identities (Vampire); the variety page shows the shortest known basis.
Identifier sb-60b657557ee8853d in the data of the bases-min seal.
Certified for
The identities
- x² ≈ x⁴
- x³yx ≈ xyx
- xyx ≈ xyx³
- xyx ≈ xy³x
- xyxy ≈ xy²x
- xyx²y ≈ xy²x²
- x²y² ≈ x²y²x²y²
- xyx²zx ≈ xyzx
- xy³zx ≈ xyzx
- xyzx ≈ xyzy²x
- xyzx ≈ xyz³x
- xyzxy ≈ xyzyx
- xyzxz ≈ xyz²x
- xyx²zy ≈ xyzyx²
- xyzx²y ≈ xyzyx²
- xyzx²z ≈ xyz²x²
- xyzy²tx ≈ xyztx
- xyz³tx ≈ xyztx
- xyztx ≈ xyztz²x
- xyztxz ≈ xyztzx
- xyzx²ty ≈ xyztyx²
- xyzx²tz ≈ xyztzx²
- xyztx²z ≈ xyztzx²
- xyztz²ux ≈ xyztux
- xyztx²uz ≈ xyztuzx²